Multiplication antidiagonal as a Finset
. #
We construct the Finset
of all pairs
of an element in s
and an element in t
that multiply to a
,
given that s
and t
are well-ordered.
theorem
Set.IsPWO.add
{α : Type u_1}
{s : Set α}
{t : Set α}
[OrderedCancelAddCommMonoid α]
(hs : s.IsPWO)
(ht : t.IsPWO)
:
(s + t).IsPWO
theorem
Set.IsPWO.mul
{α : Type u_1}
{s : Set α}
{t : Set α}
[OrderedCancelCommMonoid α]
(hs : s.IsPWO)
(ht : t.IsPWO)
:
(s * t).IsPWO
theorem
Set.IsWF.add
{α : Type u_1}
{s : Set α}
{t : Set α}
[LinearOrderedCancelAddCommMonoid α]
(hs : s.IsWF)
(ht : t.IsWF)
:
(s + t).IsWF
theorem
Set.IsWF.mul
{α : Type u_1}
{s : Set α}
{t : Set α}
[LinearOrderedCancelCommMonoid α]
(hs : s.IsWF)
(ht : t.IsWF)
:
(s * t).IsWF
theorem
Set.IsWF.min_add
{α : Type u_1}
{s : Set α}
{t : Set α}
[LinearOrderedCancelAddCommMonoid α]
(hs : s.IsWF)
(ht : t.IsWF)
(hsn : s.Nonempty)
(htn : t.Nonempty)
:
theorem
Set.IsWF.min_mul
{α : Type u_1}
{s : Set α}
{t : Set α}
[LinearOrderedCancelCommMonoid α]
(hs : s.IsWF)
(ht : t.IsWF)
(hsn : s.Nonempty)
(htn : t.Nonempty)
:
noncomputable def
Finset.addAntidiagonal
{α : Type u_1}
[OrderedCancelAddCommMonoid α]
{s : Set α}
{t : Set α}
(hs : s.IsPWO)
(ht : t.IsPWO)
(a : α)
:
Finset.addAntidiagonal hs ht a
is the set of all pairs of an element in
s
and an element in t
that add to a
, but its construction requires proofs that s
and t
are
well-ordered.
Equations
- Finset.addAntidiagonal hs ht a = ⋯.toFinset
Instances For
theorem
Finset.addAntidiagonal.proof_1
{α : Type u_1}
[OrderedCancelAddCommMonoid α]
{s : Set α}
{t : Set α}
(hs : s.IsPWO)
(ht : t.IsPWO)
(a : α)
:
(s.addAntidiagonal t a).Finite
noncomputable def
Finset.mulAntidiagonal
{α : Type u_1}
[OrderedCancelCommMonoid α]
{s : Set α}
{t : Set α}
(hs : s.IsPWO)
(ht : t.IsPWO)
(a : α)
:
Finset.mulAntidiagonal hs ht a
is the set of all pairs of an element in s
and an
element in t
that multiply to a
, but its construction requires proofs that s
and t
are
well-ordered.
Equations
- Finset.mulAntidiagonal hs ht a = ⋯.toFinset
Instances For
theorem
Finset.addAntidiagonal_mono_left
{α : Type u_1}
[OrderedCancelAddCommMonoid α]
{s : Set α}
{t : Set α}
{hs : s.IsPWO}
{ht : t.IsPWO}
{a : α}
{u : Set α}
{hu : u.IsPWO}
(h : u ⊆ s)
:
Finset.addAntidiagonal hu ht a ⊆ Finset.addAntidiagonal hs ht a
theorem
Finset.mulAntidiagonal_mono_left
{α : Type u_1}
[OrderedCancelCommMonoid α]
{s : Set α}
{t : Set α}
{hs : s.IsPWO}
{ht : t.IsPWO}
{a : α}
{u : Set α}
{hu : u.IsPWO}
(h : u ⊆ s)
:
Finset.mulAntidiagonal hu ht a ⊆ Finset.mulAntidiagonal hs ht a
theorem
Finset.addAntidiagonal_mono_right
{α : Type u_1}
[OrderedCancelAddCommMonoid α]
{s : Set α}
{t : Set α}
{hs : s.IsPWO}
{ht : t.IsPWO}
{a : α}
{u : Set α}
{hu : u.IsPWO}
(h : u ⊆ t)
:
Finset.addAntidiagonal hs hu a ⊆ Finset.addAntidiagonal hs ht a
theorem
Finset.mulAntidiagonal_mono_right
{α : Type u_1}
[OrderedCancelCommMonoid α]
{s : Set α}
{t : Set α}
{hs : s.IsPWO}
{ht : t.IsPWO}
{a : α}
{u : Set α}
{hu : u.IsPWO}
(h : u ⊆ t)
:
Finset.mulAntidiagonal hs hu a ⊆ Finset.mulAntidiagonal hs ht a
theorem
Finset.swap_mem_addAntidiagonal
{α : Type u_1}
[OrderedCancelAddCommMonoid α]
{s : Set α}
{t : Set α}
{hs : s.IsPWO}
{ht : t.IsPWO}
{a : α}
{x : α × α}
:
x.swap ∈ Finset.addAntidiagonal hs ht a ↔ x ∈ Finset.addAntidiagonal ht hs a
theorem
Finset.swap_mem_mulAntidiagonal
{α : Type u_1}
[OrderedCancelCommMonoid α]
{s : Set α}
{t : Set α}
{hs : s.IsPWO}
{ht : t.IsPWO}
{a : α}
{x : α × α}
:
x.swap ∈ Finset.mulAntidiagonal hs ht a ↔ x ∈ Finset.mulAntidiagonal ht hs a
theorem
Finset.support_addAntidiagonal_subset_add
{α : Type u_1}
[OrderedCancelAddCommMonoid α]
{s : Set α}
{t : Set α}
{hs : s.IsPWO}
{ht : t.IsPWO}
:
{a : α | (Finset.addAntidiagonal hs ht a).Nonempty} ⊆ s + t
theorem
Finset.support_mulAntidiagonal_subset_mul
{α : Type u_1}
[OrderedCancelCommMonoid α]
{s : Set α}
{t : Set α}
{hs : s.IsPWO}
{ht : t.IsPWO}
:
{a : α | (Finset.mulAntidiagonal hs ht a).Nonempty} ⊆ s * t
theorem
Finset.isPWO_support_addAntidiagonal
{α : Type u_1}
[OrderedCancelAddCommMonoid α]
{s : Set α}
{t : Set α}
{hs : s.IsPWO}
{ht : t.IsPWO}
:
{a : α | (Finset.addAntidiagonal hs ht a).Nonempty}.IsPWO
theorem
Finset.isPWO_support_mulAntidiagonal
{α : Type u_1}
[OrderedCancelCommMonoid α]
{s : Set α}
{t : Set α}
{hs : s.IsPWO}
{ht : t.IsPWO}
:
{a : α | (Finset.mulAntidiagonal hs ht a).Nonempty}.IsPWO
theorem
Finset.addAntidiagonal_min_add_min
{α : Type u_2}
[LinearOrderedCancelAddCommMonoid α]
{s : Set α}
{t : Set α}
(hs : s.IsWF)
(ht : t.IsWF)
(hns : s.Nonempty)
(hnt : t.Nonempty)
:
Finset.addAntidiagonal ⋯ ⋯ (hs.min hns + ht.min hnt) = {(hs.min hns, ht.min hnt)}
theorem
Finset.mulAntidiagonal_min_mul_min
{α : Type u_2}
[LinearOrderedCancelCommMonoid α]
{s : Set α}
{t : Set α}
(hs : s.IsWF)
(ht : t.IsWF)
(hns : s.Nonempty)
(hnt : t.Nonempty)
:
Finset.mulAntidiagonal ⋯ ⋯ (hs.min hns * ht.min hnt) = {(hs.min hns, ht.min hnt)}