Multiplication antidiagonal as a finset. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.is_pwo.mul
{α : Type u_1}
{s t : set α}
[ordered_cancel_comm_monoid α]
(hs : s.is_pwo)
(ht : t.is_pwo) :
theorem
set.is_pwo.add
{α : Type u_1}
{s t : set α}
[ordered_cancel_add_comm_monoid α]
(hs : s.is_pwo)
(ht : t.is_pwo) :
theorem
set.is_wf.add
{α : Type u_1}
{s t : set α}
[linear_ordered_cancel_add_comm_monoid α]
(hs : s.is_wf)
(ht : t.is_wf) :
theorem
set.is_wf.mul
{α : Type u_1}
{s t : set α}
[linear_ordered_cancel_comm_monoid α]
(hs : s.is_wf)
(ht : t.is_wf) :
noncomputable
def
finset.mul_antidiagonal
{α : Type u_1}
[ordered_cancel_comm_monoid α]
{s t : set α}
(hs : s.is_pwo)
(ht : t.is_pwo)
(a : α) :
finset.mul_antidiagonal_of_is_wf 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.mul_antidiagonal hs ht a = _.to_finset
noncomputable
def
finset.add_antidiagonal
{α : Type u_1}
[ordered_cancel_add_comm_monoid α]
{s t : set α}
(hs : s.is_pwo)
(ht : t.is_pwo)
(a : α) :
finset.add_antidiagonal_of_is_wf 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.add_antidiagonal hs ht a = _.to_finset
theorem
finset.mul_antidiagonal_mono_left
{α : Type u_1}
[ordered_cancel_comm_monoid α]
{s t : set α}
{hs : s.is_pwo}
{ht : t.is_pwo}
{a : α}
{u : set α}
{hu : u.is_pwo}
(h : u ⊆ s) :
finset.mul_antidiagonal hu ht a ⊆ finset.mul_antidiagonal hs ht a
theorem
finset.add_antidiagonal_mono_left
{α : Type u_1}
[ordered_cancel_add_comm_monoid α]
{s t : set α}
{hs : s.is_pwo}
{ht : t.is_pwo}
{a : α}
{u : set α}
{hu : u.is_pwo}
(h : u ⊆ s) :
finset.add_antidiagonal hu ht a ⊆ finset.add_antidiagonal hs ht a
theorem
finset.mul_antidiagonal_mono_right
{α : Type u_1}
[ordered_cancel_comm_monoid α]
{s t : set α}
{hs : s.is_pwo}
{ht : t.is_pwo}
{a : α}
{u : set α}
{hu : u.is_pwo}
(h : u ⊆ t) :
finset.mul_antidiagonal hs hu a ⊆ finset.mul_antidiagonal hs ht a
theorem
finset.add_antidiagonal_mono_right
{α : Type u_1}
[ordered_cancel_add_comm_monoid α]
{s t : set α}
{hs : s.is_pwo}
{ht : t.is_pwo}
{a : α}
{u : set α}
{hu : u.is_pwo}
(h : u ⊆ t) :
finset.add_antidiagonal hs hu a ⊆ finset.add_antidiagonal hs ht a
@[simp]
theorem
finset.swap_mem_mul_antidiagonal
{α : Type u_1}
[ordered_cancel_comm_monoid α]
{s t : set α}
{hs : s.is_pwo}
{ht : t.is_pwo}
{a : α}
{x : α × α} :
x.swap ∈ finset.mul_antidiagonal hs ht a ↔ x ∈ finset.mul_antidiagonal ht hs a
@[simp]
theorem
finset.swap_mem_add_antidiagonal
{α : Type u_1}
[ordered_cancel_add_comm_monoid α]
{s t : set α}
{hs : s.is_pwo}
{ht : t.is_pwo}
{a : α}
{x : α × α} :
x.swap ∈ finset.add_antidiagonal hs ht a ↔ x ∈ finset.add_antidiagonal ht hs a
theorem
finset.support_add_antidiagonal_subset_add
{α : Type u_1}
[ordered_cancel_add_comm_monoid α]
{s t : set α}
{hs : s.is_pwo}
{ht : t.is_pwo} :
{a : α | (finset.add_antidiagonal hs ht a).nonempty} ⊆ s + t
theorem
finset.support_mul_antidiagonal_subset_mul
{α : Type u_1}
[ordered_cancel_comm_monoid α]
{s t : set α}
{hs : s.is_pwo}
{ht : t.is_pwo} :
{a : α | (finset.mul_antidiagonal hs ht a).nonempty} ⊆ s * t
theorem
finset.is_pwo_support_add_antidiagonal
{α : Type u_1}
[ordered_cancel_add_comm_monoid α]
{s t : set α}
{hs : s.is_pwo}
{ht : t.is_pwo} :
{a : α | (finset.add_antidiagonal hs ht a).nonempty}.is_pwo
theorem
finset.is_pwo_support_mul_antidiagonal
{α : Type u_1}
[ordered_cancel_comm_monoid α]
{s t : set α}
{hs : s.is_pwo}
{ht : t.is_pwo} :
{a : α | (finset.mul_antidiagonal hs ht a).nonempty}.is_pwo