Documentation

Mathlib.Data.Finset.SMulAntidiagonal

Antidiagonal for scalar multiplication as a Finset. #

Given partially ordered sets G and P, with an action of G on P that preserves and reflects the order relation, we construct, for any element a in P and partially well-ordered subsets s in G and t in P, the Finset of all pairs of an element in s and an element in t that scalar-multiply to a.

Definitions #

theorem Set.IsPWO.vadd {G : Type u_1} {P : Type u_2} [PartialOrder G] [PartialOrder P] [VAdd G P] [IsOrderedCancelVAdd G P] {s : Set G} {t : Set P} (hs : s.IsPWO) (ht : t.IsPWO) :
(s +ᵥ t).IsPWO
theorem Set.IsPWO.smul {G : Type u_1} {P : Type u_2} [PartialOrder G] [PartialOrder P] [SMul G P] [IsOrderedCancelSMul G P] {s : Set G} {t : Set P} (hs : s.IsPWO) (ht : t.IsPWO) :
(s t).IsPWO
theorem Set.IsWF.vadd {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) :
(s +ᵥ t).IsWF
theorem Set.IsWF.smul {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) :
(s t).IsWF
theorem Set.IsWF.min_vadd {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) (hsn : s.Nonempty) (htn : t.Nonempty) :
.min = hs.min hsn +ᵥ ht.min htn
theorem Set.IsWF.min_smul {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) (hsn : s.Nonempty) (htn : t.Nonempty) :
.min = hs.min hsn ht.min htn
noncomputable def Finset.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) :
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.

Equations
Instances For
    noncomputable def Finset.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) :
    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 proofs that s and t are well-ordered.

    Equations
    Instances For
      @[simp]
      theorem Finset.mem_vaddAntidiagonal {G : Type u_1} {P : Type u_2} [PartialOrder G] [PartialOrder P] [VAdd G P] [IsOrderedCancelVAdd G P] {s : Set G} {t : Set P} (hs : s.IsPWO) (ht : t.IsPWO) (a : P) {x : G × P} :
      x Finset.VAddAntidiagonal hs ht a x.1 s x.2 t x.1 +ᵥ x.2 = a
      @[simp]
      theorem Finset.mem_smulAntidiagonal {G : Type u_1} {P : Type u_2} [PartialOrder G] [PartialOrder P] [SMul G P] [IsOrderedCancelSMul G P] {s : Set G} {t : Set P} (hs : s.IsPWO) (ht : t.IsPWO) (a : P) {x : G × P} :
      x Finset.SMulAntidiagonal hs ht a x.1 s x.2 t x.1 x.2 = a
      theorem Finset.vaddAntidiagonal_mono_left {G : Type u_1} {P : Type u_2} [PartialOrder G] [PartialOrder P] [VAdd G P] [IsOrderedCancelVAdd G P] {s : Set G} {t : Set P} {u : Set G} {hu : u.IsPWO} {a : P} {hs : s.IsPWO} {ht : t.IsPWO} (h : u s) :
      theorem Finset.smulAntidiagonal_mono_left {G : Type u_1} {P : Type u_2} [PartialOrder G] [PartialOrder P] [SMul G P] [IsOrderedCancelSMul G P] {s : Set G} {t : Set P} {u : Set G} {hu : u.IsPWO} {a : P} {hs : s.IsPWO} {ht : t.IsPWO} (h : u s) :
      theorem Finset.vaddAntidiagonal_mono_right {G : Type u_1} {P : Type u_2} [PartialOrder G] [PartialOrder P] [VAdd G P] [IsOrderedCancelVAdd G P] {s : Set G} {t : Set P} {v : Set P} {hv : v.IsPWO} {a : P} {hs : s.IsPWO} {ht : t.IsPWO} (h : v t) :
      theorem Finset.smulAntidiagonal_mono_right {G : Type u_1} {P : Type u_2} [PartialOrder G] [PartialOrder P] [SMul G P] [IsOrderedCancelSMul G P] {s : Set G} {t : Set P} {v : Set P} {hv : v.IsPWO} {a : P} {hs : s.IsPWO} {ht : t.IsPWO} (h : v t) :
      theorem Finset.support_vaddAntidiagonal_subset_vadd {G : Type u_1} {P : Type u_2} [PartialOrder G] [PartialOrder P] [VAdd G P] [IsOrderedCancelVAdd G P] {s : Set G} {t : Set P} {hs : s.IsPWO} {ht : t.IsPWO} :
      {a : P | (Finset.VAddAntidiagonal hs ht a).Nonempty} s +ᵥ t
      theorem Finset.support_smulAntidiagonal_subset_smul {G : Type u_1} {P : Type u_2} [PartialOrder G] [PartialOrder P] [SMul G P] [IsOrderedCancelSMul G P] {s : Set G} {t : Set P} {hs : s.IsPWO} {ht : t.IsPWO} :
      {a : P | (Finset.SMulAntidiagonal hs ht a).Nonempty} s t
      theorem Finset.isPWO_support_vaddAntidiagonal {G : Type u_1} {P : Type u_2} [PartialOrder G] [PartialOrder P] [VAdd G P] [IsOrderedCancelVAdd G P] {s : Set G} {t : Set P} {hs : s.IsPWO} {ht : t.IsPWO} :
      {a : P | (Finset.VAddAntidiagonal hs ht a).Nonempty}.IsPWO
      theorem Finset.isPWO_support_smulAntidiagonal {G : Type u_1} {P : Type u_2} [PartialOrder G] [PartialOrder P] [SMul G P] [IsOrderedCancelSMul G P] {s : Set G} {t : Set P} {hs : s.IsPWO} {ht : t.IsPWO} :
      {a : P | (Finset.SMulAntidiagonal hs ht a).Nonempty}.IsPWO
      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) :
      Finset.VAddAntidiagonal (hs.min hns +ᵥ ht.min hnt) = {(hs.min hns, ht.min hnt)}
      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) :
      Finset.SMulAntidiagonal (hs.min hns ht.min hnt) = {(hs.min hns, ht.min hnt)}