Multiplication antidiagonal #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
theorem
set.mul_antidiagonal_mono_left
{α : Type u_1}
[has_mul α]
{s₁ s₂ t : set α}
{a : α}
(h : s₁ ⊆ s₂) :
s₁.mul_antidiagonal t a ⊆ s₂.mul_antidiagonal t a
theorem
set.add_antidiagonal_mono_left
{α : Type u_1}
[has_add α]
{s₁ s₂ t : set α}
{a : α}
(h : s₁ ⊆ s₂) :
s₁.add_antidiagonal t a ⊆ s₂.add_antidiagonal t a
theorem
set.mul_antidiagonal_mono_right
{α : Type u_1}
[has_mul α]
{s t₁ t₂ : set α}
{a : α}
(h : t₁ ⊆ t₂) :
s.mul_antidiagonal t₁ a ⊆ s.mul_antidiagonal t₂ a
theorem
set.add_antidiagonal_mono_right
{α : Type u_1}
[has_add α]
{s t₁ t₂ : set α}
{a : α}
(h : t₁ ⊆ t₂) :
s.add_antidiagonal t₁ a ⊆ s.add_antidiagonal t₂ a
@[simp]
theorem
set.swap_mem_mul_antidiagonal
{α : Type u_1}
[comm_semigroup α]
{s t : set α}
{a : α}
{x : α × α} :
x.swap ∈ s.mul_antidiagonal t a ↔ x ∈ t.mul_antidiagonal s a
@[simp]
theorem
set.swap_mem_add_antidiagonal
{α : Type u_1}
[add_comm_semigroup α]
{s t : set α}
{a : α}
{x : α × α} :
x.swap ∈ s.add_antidiagonal t a ↔ x ∈ t.add_antidiagonal s a
theorem
set.add_antidiagonal.eq_of_fst_eq_fst
{α : Type u_1}
[add_cancel_comm_monoid α]
{s t : set α}
{a : α}
{x y : ↥(s.add_antidiagonal t a)}
(h : ↑x.fst = ↑y.fst) :
x = y
theorem
set.mul_antidiagonal.eq_of_fst_eq_fst
{α : Type u_1}
[cancel_comm_monoid α]
{s t : set α}
{a : α}
{x y : ↥(s.mul_antidiagonal t a)}
(h : ↑x.fst = ↑y.fst) :
x = y
theorem
set.add_antidiagonal.eq_of_snd_eq_snd
{α : Type u_1}
[add_cancel_comm_monoid α]
{s t : set α}
{a : α}
{x y : ↥(s.add_antidiagonal t a)}
(h : ↑x.snd = ↑y.snd) :
x = y
theorem
set.mul_antidiagonal.eq_of_snd_eq_snd
{α : Type u_1}
[cancel_comm_monoid α]
{s t : set α}
{a : α}
{x y : ↥(s.mul_antidiagonal t a)}
(h : ↑x.snd = ↑y.snd) :
x = y
theorem
set.mul_antidiagonal.finite_of_is_pwo
{α : Type u_1}
[ordered_cancel_comm_monoid α]
{s t : set α}
(hs : s.is_pwo)
(ht : t.is_pwo)
(a : α) :
(s.mul_antidiagonal t a).finite
theorem
set.add_antidiagonal.finite_of_is_pwo
{α : Type u_1}
[ordered_cancel_add_comm_monoid α]
{s t : set α}
(hs : s.is_pwo)
(ht : t.is_pwo)
(a : α) :
(s.add_antidiagonal t a).finite
theorem
set.add_antidiagonal.finite_of_is_wf
{α : Type u_1}
[linear_ordered_cancel_add_comm_monoid α]
{s t : set α}
(hs : s.is_wf)
(ht : t.is_wf)
(a : α) :
(s.add_antidiagonal t a).finite
theorem
set.mul_antidiagonal.finite_of_is_wf
{α : Type u_1}
[linear_ordered_cancel_comm_monoid α]
{s t : set α}
(hs : s.is_wf)
(ht : t.is_wf)
(a : α) :
(s.mul_antidiagonal t a).finite