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

• Finset.SMulAntidiagonal : Finset antidiagonal for PWO inputs.
• Finset.VAddAntidiagonal : Finset antidiagonal for PWO inputs.

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

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

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

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

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

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

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

• Finset.SMulAntidiagonal hs ht a = ⋯.toFinset

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

• Finset.VAddAntidiagonal hs ht a = ⋯.toFinset

@[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 ∈ SMulAntidiagonal hs ht a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a

@[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 ∈ VAddAntidiagonal hs ht a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 +ᵥ x.2 = a

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) : SMulAntidiagonal hu ht a ⊆ SMulAntidiagonal hs ht 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) : VAddAntidiagonal hu ht a ⊆ VAddAntidiagonal hs ht a

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 v : Set P} {hv : v.IsPWO} {a : P} {hs : s.IsPWO} {ht : t.IsPWO} (h : v ⊆ t) : SMulAntidiagonal hs hv a ⊆ SMulAntidiagonal hs ht a

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 v : Set P} {hv : v.IsPWO} {a : P} {hs : s.IsPWO} {ht : t.IsPWO} (h : v ⊆ t) : VAddAntidiagonal hs hv a ⊆ VAddAntidiagonal hs ht a

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 | (SMulAntidiagonal hs ht a).Nonempty} ⊆ s • 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 | (VAddAntidiagonal hs ht a).Nonempty} ⊆ s +ᵥ t

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 | (SMulAntidiagonal hs ht a).Nonempty}.IsPWO

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 | (VAddAntidiagonal hs ht a).Nonempty}.IsPWO

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)}

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)}