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}
[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.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.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.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.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)
:
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)
:
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.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
Instances For
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.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
Instances For
@[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}
:
@[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}
:
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)
:
Finset.SMulAntidiagonal hu ht a ⊆ Finset.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)
:
Finset.VAddAntidiagonal hu ht a ⊆ Finset.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)
:
Finset.SMulAntidiagonal hs hv a ⊆ Finset.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)
:
Finset.VAddAntidiagonal hs hv a ⊆ Finset.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 | (Finset.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 | (Finset.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 | (Finset.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 | (Finset.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)
:
Finset.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)
:
Finset.VAddAntidiagonal ⋯ ⋯ (hs.min hns +ᵥ ht.min hnt) = {(hs.min hns, ht.min hnt)}