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 : Set.IsPwo s)
(ht : Set.IsPwo t)
:
theorem
Set.IsPwo.mul
{α : Type u_1}
{s : Set α}
{t : Set α}
[OrderedCancelCommMonoid α]
(hs : Set.IsPwo s)
(ht : Set.IsPwo t)
:
theorem
Set.IsWf.add
{α : Type u_1}
{s : Set α}
{t : Set α}
[LinearOrderedCancelAddCommMonoid α]
(hs : Set.IsWf s)
(ht : Set.IsWf t)
:
theorem
Set.IsWf.mul
{α : Type u_1}
{s : Set α}
{t : Set α}
[LinearOrderedCancelCommMonoid α]
(hs : Set.IsWf s)
(ht : Set.IsWf t)
:
theorem
Set.IsWf.min_add
{α : Type u_1}
{s : Set α}
{t : Set α}
[LinearOrderedCancelAddCommMonoid α]
(hs : Set.IsWf s)
(ht : Set.IsWf t)
(hsn : Set.Nonempty s)
(htn : Set.Nonempty t)
:
Set.IsWf.min (_ : Set.IsWf (s + t)) (_ : Set.Nonempty (s + t)) = Set.IsWf.min hs hsn + Set.IsWf.min ht htn
theorem
Set.IsWf.min_mul
{α : Type u_1}
{s : Set α}
{t : Set α}
[LinearOrderedCancelCommMonoid α]
(hs : Set.IsWf s)
(ht : Set.IsWf t)
(hsn : Set.Nonempty s)
(htn : Set.Nonempty t)
:
Set.IsWf.min (_ : Set.IsWf (s * t)) (_ : Set.Nonempty (s * t)) = Set.IsWf.min hs hsn * Set.IsWf.min ht htn
noncomputable def
Finset.addAntidiagonal
{α : Type u_1}
[OrderedCancelAddCommMonoid α]
{s : Set α}
{t : Set α}
(hs : Set.IsPwo s)
(ht : Set.IsPwo t)
(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 = Set.Finite.toFinset (_ : Set.Finite (Set.addAntidiagonal s t a))
Instances For
noncomputable def
Finset.mulAntidiagonal
{α : Type u_1}
[OrderedCancelCommMonoid α]
{s : Set α}
{t : Set α}
(hs : Set.IsPwo s)
(ht : Set.IsPwo t)
(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 = Set.Finite.toFinset (_ : Set.Finite (Set.mulAntidiagonal s t a))
Instances For
theorem
Finset.addAntidiagonal_mono_left
{α : Type u_1}
[OrderedCancelAddCommMonoid α]
{s : Set α}
{t : Set α}
{hs : Set.IsPwo s}
{ht : Set.IsPwo t}
{a : α}
{u : Set α}
{hu : Set.IsPwo u}
(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 : Set.IsPwo s}
{ht : Set.IsPwo t}
{a : α}
{u : Set α}
{hu : Set.IsPwo u}
(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 : Set.IsPwo s}
{ht : Set.IsPwo t}
{a : α}
{u : Set α}
{hu : Set.IsPwo u}
(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 : Set.IsPwo s}
{ht : Set.IsPwo t}
{a : α}
{u : Set α}
{hu : Set.IsPwo u}
(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 : Set.IsPwo s}
{ht : Set.IsPwo t}
{a : α}
{x : α × α}
:
Prod.swap x ∈ 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 : Set.IsPwo s}
{ht : Set.IsPwo t}
{a : α}
{x : α × α}
:
Prod.swap x ∈ Finset.mulAntidiagonal hs ht a ↔ x ∈ Finset.mulAntidiagonal ht hs a
abbrev
Finset.support_addAntidiagonal_subset_add.match_1
{α : Type u_1}
[OrderedCancelAddCommMonoid α]
{s : Set α}
{t : Set α}
{hs : Set.IsPwo s}
{ht : Set.IsPwo t}
(a : α)
(motive : a ∈ {a | Finset.Nonempty (Finset.addAntidiagonal hs ht a)} → Prop)
:
(x : a ∈ {a | Finset.Nonempty (Finset.addAntidiagonal hs ht a)}) →
((b : α × α) → (hb : b ∈ Finset.addAntidiagonal hs ht a) → motive (_ : ∃ x, x ∈ Finset.addAntidiagonal hs ht a)) →
motive x
Equations
- Finset.support_addAntidiagonal_subset_add.match_1 a motive x h_1 = Exists.casesOn x fun w h => h_1 w h
Instances For
theorem
Finset.support_addAntidiagonal_subset_add
{α : Type u_1}
[OrderedCancelAddCommMonoid α]
{s : Set α}
{t : Set α}
{hs : Set.IsPwo s}
{ht : Set.IsPwo t}
:
{a | Finset.Nonempty (Finset.addAntidiagonal hs ht a)} ⊆ s + t
theorem
Finset.support_mulAntidiagonal_subset_mul
{α : Type u_1}
[OrderedCancelCommMonoid α]
{s : Set α}
{t : Set α}
{hs : Set.IsPwo s}
{ht : Set.IsPwo t}
:
{a | Finset.Nonempty (Finset.mulAntidiagonal hs ht a)} ⊆ s * t
theorem
Finset.isPwo_support_addAntidiagonal
{α : Type u_1}
[OrderedCancelAddCommMonoid α]
{s : Set α}
{t : Set α}
{hs : Set.IsPwo s}
{ht : Set.IsPwo t}
:
Set.IsPwo {a | Finset.Nonempty (Finset.addAntidiagonal hs ht a)}
theorem
Finset.isPwo_support_mulAntidiagonal
{α : Type u_1}
[OrderedCancelCommMonoid α]
{s : Set α}
{t : Set α}
{hs : Set.IsPwo s}
{ht : Set.IsPwo t}
:
Set.IsPwo {a | Finset.Nonempty (Finset.mulAntidiagonal hs ht a)}
theorem
Finset.addAntidiagonal_min_add_min
{α : Type u_2}
[LinearOrderedCancelAddCommMonoid α]
{s : Set α}
{t : Set α}
(hs : Set.IsWf s)
(ht : Set.IsWf t)
(hns : Set.Nonempty s)
(hnt : Set.Nonempty t)
:
Finset.addAntidiagonal (_ : Set.IsPwo s) (_ : Set.IsPwo t) (Set.IsWf.min hs hns + Set.IsWf.min ht hnt) = {(Set.IsWf.min hs hns, Set.IsWf.min ht hnt)}
theorem
Finset.mulAntidiagonal_min_mul_min
{α : Type u_2}
[LinearOrderedCancelCommMonoid α]
{s : Set α}
{t : Set α}
(hs : Set.IsWf s)
(ht : Set.IsWf t)
(hns : Set.Nonempty s)
(hnt : Set.Nonempty t)
:
Finset.mulAntidiagonal (_ : Set.IsPwo s) (_ : Set.IsPwo t) (Set.IsWf.min hs hns * Set.IsWf.min ht hnt) = {(Set.IsWf.min hs hns, Set.IsWf.min ht hnt)}