Documentation

Mathlib.Data.Finset.SMulAntidiagonal

Antidiagonal for scalar multiplication as a Finset. #

Given sets G and P, with an action of G on P, we construct, for any element a in P, the Finset of all pairs of an element in s and an element in t that scalar-multiply to a, assuming that set is finite.

Definitions #

source
theorem Set.IsPWO.smul {G : Type u_1} {P : Type u_2} [Preorder G] [Preorder P] [SMul G P] [IsOrderedSMul G P] {s : Set G} {t : Set P} (hs : s.IsPWO) (ht : t.IsPWO) :
(s • t).IsPWO
source
theorem Set.IsPWO.vadd {G : Type u_1} {P : Type u_2} [Preorder G] [Preorder P] [VAdd G P] [IsOrderedVAdd G P] {s : Set G} {t : Set P} (hs : s.IsPWO) (ht : t.IsPWO) :
(s +ᵥ t).IsPWO
source
theorem Set.IsWF.smul {G : Type u_1} {P : Type u_2} [LinearOrder G] [LinearOrder P] [SMul G P] [IsOrderedSMul G P] {s : Set G} {t : Set P} (hs : s.IsWF) (ht : t.IsWF) :
(s • t).IsWF
source
theorem Set.IsWF.vadd {G : Type u_1} {P : Type u_2} [LinearOrder G] [LinearOrder P] [VAdd G P] [IsOrderedVAdd G P] {s : Set G} {t : Set P} (hs : s.IsWF) (ht : t.IsWF) :
(s +ᵥ t).IsWF
source
theorem Set.IsWF.min_smul {G : Type u_1} {P : Type u_2} [LinearOrder G] [LinearOrder P] [SMul G P] [IsOrderedSMul G P] {s : Set G} {t : Set P} (hs : s.IsWF) (ht : t.IsWF) (hsn : s.Nonempty) (htn : t.Nonempty) :
⋯.min ⋯ = hs.min hsn • ht.min htn
source
theorem Set.IsWF.min_vadd {G : Type u_1} {P : Type u_2} [LinearOrder G] [LinearOrder P] [VAdd G P] [IsOrderedVAdd G P] {s : Set G} {t : Set P} (hs : s.IsWF) (ht : t.IsWF) (hsn : s.Nonempty) (htn : t.Nonempty) :
⋯.min ⋯ = hs.min hsn +ᵥ ht.min htn
source
noncomputable def Finset.SMulAntidiagonal {G : Type u_1} {P : Type u_2} [SMul G P] {s : Set G} {t : Set P} (a : P) (h : (s.smulAntidiagonal t a).Finite) :
Finset (G × P)

Finset.SMulAntidiagonal hs ht a is the set of all pairs of an element in s and an element in t whose scalar multiplication yields a, but its construction requires a proof that the set-theoretic antidiagonal is finite.

Instances For
    source
    noncomputable def Finset.VAddAntidiagonal {G : Type u_1} {P : Type u_2} [VAdd G P] {s : Set G} {t : Set P} (a : P) (h : (s.vaddAntidiagonal t a).Finite) :
    Finset (G × P)

    Finset.VAddAntidiagonal hs ht a is the set of all pairs of an element in s and an element in t whose vector addition yields a, but its construction requires proofs that s and t are well-ordered.

    Instances For
      source
      @[simp]
      theorem Finset.mem_smulAntidiagonal {G : Type u_1} {P : Type u_2} [SMul G P] {s : Set G} {t : Set P} (a : P) (h : (s.smulAntidiagonal t a).Finite) {x : G × P} :
      x ∈ SMulAntidiagonal a h ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a
      source
      @[simp]
      theorem Finset.mem_vaddAntidiagonal {G : Type u_1} {P : Type u_2} [VAdd G P] {s : Set G} {t : Set P} (a : P) (h : (s.vaddAntidiagonal t a).Finite) {x : G × P} :
      x ∈ VAddAntidiagonal a h ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 +ᵥ x.2 = a
      source
      theorem Finset.smulAntidiagonal_mono_left {G : Type u_1} {P : Type u_2} [SMul G P] {s u : Set G} {t : Set P} (a : P) (h : u ⊆ s) (hst : (s.smulAntidiagonal t a).Finite) (hut : (u.smulAntidiagonal t a).Finite) :
      SMulAntidiagonal a hut ⊆ SMulAntidiagonal a hst
      source
      theorem Finset.vaddAntidiagonal_mono_left {G : Type u_1} {P : Type u_2} [VAdd G P] {s u : Set G} {t : Set P} (a : P) (h : u ⊆ s) (hst : (s.vaddAntidiagonal t a).Finite) (hut : (u.vaddAntidiagonal t a).Finite) :
      VAddAntidiagonal a hut ⊆ VAddAntidiagonal a hst
      source
      theorem Finset.smulAntidiagonal_mono_right {G : Type u_1} {P : Type u_2} [SMul G P] {s : Set G} {t v : Set P} (a : P) (hst : (s.smulAntidiagonal t a).Finite) (hsv : (s.smulAntidiagonal v a).Finite) (h : v ⊆ t) :
      SMulAntidiagonal a hsv ⊆ SMulAntidiagonal a hst
      source
      theorem Finset.vaddAntidiagonal_mono_right {G : Type u_1} {P : Type u_2} [VAdd G P] {s : Set G} {t v : Set P} (a : P) (hst : (s.vaddAntidiagonal t a).Finite) (hsv : (s.vaddAntidiagonal v a).Finite) (h : v ⊆ t) :
      VAddAntidiagonal a hsv ⊆ VAddAntidiagonal a hst
      source
      theorem Finset.support_smulAntidiagonal_subset_smul {G : Type u_1} {P : Type u_2} [SMul G P] {s : Set G} {t : Set P} (hst : ∀ (a : P), (s.smulAntidiagonal t a).Finite) :
      {a : P | (SMulAntidiagonal a ⋯).Nonempty} ⊆ s • t
      source
      theorem Finset.support_vaddAntidiagonal_subset_vadd {G : Type u_1} {P : Type u_2} [VAdd G P] {s : Set G} {t : Set P} (hst : ∀ (a : P), (s.vaddAntidiagonal t a).Finite) :
      {a : P | (VAddAntidiagonal a ⋯).Nonempty} ⊆ s +ᵥ t
      source
      theorem Finset.isPWO_support_smulAntidiagonal {G : Type u_1} {P : Type u_2} [SMul G P] [PartialOrder G] [PartialOrder P] [IsOrderedCancelSMul G P] {s : Set G} {t : Set P} (hs : s.IsPWO) (ht : t.IsPWO) :
      {a : P | (SMulAntidiagonal a ⋯).Nonempty}.IsPWO
      source
      theorem Finset.isPWO_support_vaddAntidiagonal {G : Type u_1} {P : Type u_2} [VAdd G P] [PartialOrder G] [PartialOrder P] [IsOrderedCancelVAdd G P] {s : Set G} {t : Set P} (hs : s.IsPWO) (ht : t.IsPWO) :
      {a : P | (VAddAntidiagonal a ⋯).Nonempty}.IsPWO
      source
      theorem Finset.smulAntidiagonal_min_smul_min {G : Type u_1} {P : Type u_2} [LinearOrder G] [LinearOrder P] [SMul G P] [IsOrderedCancelSMul G P] {s : Set G} {t : Set P} (hs : s.IsWF) (ht : t.IsWF) (hns : s.Nonempty) (hnt : t.Nonempty) :
      SMulAntidiagonal (hs.min hns • ht.min hnt) ⋯ = {(hs.min hns, ht.min hnt)}
      source
      theorem Finset.vaddAntidiagonal_min_vadd_min {G : Type u_1} {P : Type u_2} [LinearOrder G] [LinearOrder P] [VAdd G P] [IsOrderedCancelVAdd G P] {s : Set G} {t : Set P} (hs : s.IsWF) (ht : t.IsWF) (hns : s.Nonempty) (hnt : t.Nonempty) :
      VAddAntidiagonal (hs.min hns +ᵥ ht.min hnt) ⋯ = {(hs.min hns, ht.min hnt)}