mathlib3documentation

data.finset.mul_antidiagonal

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 α} (hs : s.is_pwo) (ht : t.is_pwo) :
(s * t).is_pwo
theorem set.is_pwo.add {α : Type u_1} {s t : set α} (hs : s.is_pwo) (ht : t.is_pwo) :
(s + t).is_pwo
theorem set.is_wf.add {α : Type u_1} {s t : set α} (hs : s.is_wf) (ht : t.is_wf) :
(s + t).is_wf
theorem set.is_wf.mul {α : Type u_1} {s t : set α} (hs : s.is_wf) (ht : t.is_wf) :
(s * t).is_wf
theorem set.is_wf.min_add {α : Type u_1} {s t : set α} (hs : s.is_wf) (ht : t.is_wf) (hsn : s.nonempty) (htn : t.nonempty) :
_.min _ = hs.min hsn + ht.min htn
theorem set.is_wf.min_mul {α : Type u_1} {s t : set α} (hs : s.is_wf) (ht : t.is_wf) (hsn : s.nonempty) (htn : t.nonempty) :
_.min _ = hs.min hsn * ht.min htn
noncomputable def finset.mul_antidiagonal {α : Type u_1} {s t : set α} (hs : s.is_pwo) (ht : t.is_pwo) (a : α) :
finset × α)

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
noncomputable def finset.add_antidiagonal {α : Type u_1} {s t : set α} (hs : s.is_pwo) (ht : t.is_pwo) (a : α) :
finset × α)

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
@[simp]
theorem finset.mem_mul_antidiagonal {α : Type u_1} {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} {a : α} {x : α × α} :
x a x.fst s x.snd t x.fst * x.snd = a
@[simp]
theorem finset.mem_add_antidiagonal {α : Type u_1} {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} {a : α} {x : α × α} :
x a x.fst s x.snd t x.fst + x.snd = a
theorem finset.mul_antidiagonal_mono_left {α : Type u_1} {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} {a : α} {u : set α} {hu : u.is_pwo} (h : u s) :
a a
theorem finset.add_antidiagonal_mono_left {α : Type u_1} {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} {a : α} {u : set α} {hu : u.is_pwo} (h : u s) :
a a
theorem finset.mul_antidiagonal_mono_right {α : Type u_1} {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} {a : α} {u : set α} {hu : u.is_pwo} (h : u t) :
a a
theorem finset.add_antidiagonal_mono_right {α : Type u_1} {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} {a : α} {u : set α} {hu : u.is_pwo} (h : u t) :
a a
@[simp]
theorem finset.swap_mem_mul_antidiagonal {α : Type u_1} {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} {a : α} {x : α × α} :
x.swap a x a
@[simp]
theorem finset.swap_mem_add_antidiagonal {α : Type u_1} {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} {a : α} {x : α × α} :
x.swap a x a
theorem finset.support_add_antidiagonal_subset_add {α : Type u_1} {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} :
{a : α | ht a).nonempty} s + t
theorem finset.support_mul_antidiagonal_subset_mul {α : Type u_1} {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} :
{a : α | ht a).nonempty} s * t
theorem finset.is_pwo_support_add_antidiagonal {α : Type u_1} {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} :
{a : α | ht a).nonempty}.is_pwo
theorem finset.is_pwo_support_mul_antidiagonal {α : Type u_1} {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} :
{a : α | ht a).nonempty}.is_pwo
theorem finset.add_antidiagonal_min_add_min {α : Type u_1} {s t : set α} (hs : s.is_wf) (ht : t.is_wf) (hns : s.nonempty) (hnt : t.nonempty) :
(hs.min hns + ht.min hnt) = {(hs.min hns, ht.min hnt)}
theorem finset.mul_antidiagonal_min_mul_min {α : Type u_1} {s t : set α} (hs : s.is_wf) (ht : t.is_wf) (hns : s.nonempty) (hnt : t.nonempty) :
(hs.min hns * ht.min hnt) = {(hs.min hns, ht.min hnt)}