Multiplication antidiagonal #
Set.mulAntidiagonal s t a is the set of all pairs of an element in s and an element in t
that multiply to a.
Instances For
theorem
Set.addAntidiagonal_mono_left
{α : Type u_1}
[Add α]
{s₁ : Set α}
{s₂ : Set α}
{t : Set α}
{a : α}
(h : s₁ ⊆ s₂)
:
Set.addAntidiagonal s₁ t a ⊆ Set.addAntidiagonal s₂ t a
theorem
Set.mulAntidiagonal_mono_left
{α : Type u_1}
[Mul α]
{s₁ : Set α}
{s₂ : Set α}
{t : Set α}
{a : α}
(h : s₁ ⊆ s₂)
:
Set.mulAntidiagonal s₁ t a ⊆ Set.mulAntidiagonal s₂ t a
theorem
Set.addAntidiagonal_mono_right
{α : Type u_1}
[Add α]
{s : Set α}
{t₁ : Set α}
{t₂ : Set α}
{a : α}
(h : t₁ ⊆ t₂)
:
Set.addAntidiagonal s t₁ a ⊆ Set.addAntidiagonal s t₂ a
theorem
Set.mulAntidiagonal_mono_right
{α : Type u_1}
[Mul α]
{s : Set α}
{t₁ : Set α}
{t₂ : Set α}
{a : α}
(h : t₁ ⊆ t₂)
:
Set.mulAntidiagonal s t₁ a ⊆ Set.mulAntidiagonal s t₂ a
theorem
Set.swap_mem_addAntidiagonal
{α : Type u_1}
[AddCommSemigroup α]
{s : Set α}
{t : Set α}
{a : α}
{x : α × α}
:
Prod.swap x ∈ Set.addAntidiagonal s t a ↔ x ∈ Set.addAntidiagonal t s a
theorem
Set.swap_mem_mulAntidiagonal
{α : Type u_1}
[CommSemigroup α]
{s : Set α}
{t : Set α}
{a : α}
{x : α × α}
:
Prod.swap x ∈ Set.mulAntidiagonal s t a ↔ x ∈ Set.mulAntidiagonal t s a
theorem
Set.AddAntidiagonal.fst_eq_fst_iff_snd_eq_snd
{α : Type u_1}
[AddCancelCommMonoid α]
{s : Set α}
{t : Set α}
{a : α}
{x : ↑(Set.addAntidiagonal s t a)}
{y : ↑(Set.addAntidiagonal s t a)}
:
theorem
Set.MulAntidiagonal.fst_eq_fst_iff_snd_eq_snd
{α : Type u_1}
[CancelCommMonoid α]
{s : Set α}
{t : Set α}
{a : α}
{x : ↑(Set.mulAntidiagonal s t a)}
{y : ↑(Set.mulAntidiagonal s t a)}
:
theorem
Set.AddAntidiagonal.eq_of_fst_eq_fst
{α : Type u_1}
[AddCancelCommMonoid α]
{s : Set α}
{t : Set α}
{a : α}
{x : ↑(Set.addAntidiagonal s t a)}
{y : ↑(Set.addAntidiagonal s t a)}
(h : (↑x).fst = (↑y).fst)
:
x = y
theorem
Set.MulAntidiagonal.eq_of_fst_eq_fst
{α : Type u_1}
[CancelCommMonoid α]
{s : Set α}
{t : Set α}
{a : α}
{x : ↑(Set.mulAntidiagonal s t a)}
{y : ↑(Set.mulAntidiagonal s t a)}
(h : (↑x).fst = (↑y).fst)
:
x = y
theorem
Set.AddAntidiagonal.eq_of_snd_eq_snd
{α : Type u_1}
[AddCancelCommMonoid α]
{s : Set α}
{t : Set α}
{a : α}
{x : ↑(Set.addAntidiagonal s t a)}
{y : ↑(Set.addAntidiagonal s t a)}
(h : (↑x).snd = (↑y).snd)
:
x = y
theorem
Set.MulAntidiagonal.eq_of_snd_eq_snd
{α : Type u_1}
[CancelCommMonoid α]
{s : Set α}
{t : Set α}
{a : α}
{x : ↑(Set.mulAntidiagonal s t a)}
{y : ↑(Set.mulAntidiagonal s t a)}
(h : (↑x).snd = (↑y).snd)
:
x = y
theorem
Set.AddAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd
{α : Type u_1}
[OrderedCancelAddCommMonoid α]
(s : Set α)
(t : Set α)
(a : α)
{x : ↑(Set.addAntidiagonal s t a)}
{y : ↑(Set.addAntidiagonal s t a)}
(h₁ : (↑x).fst ≤ (↑y).fst)
(h₂ : (↑x).snd ≤ (↑y).snd)
:
x = y
theorem
Set.MulAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd
{α : Type u_1}
[OrderedCancelCommMonoid α]
(s : Set α)
(t : Set α)
(a : α)
{x : ↑(Set.mulAntidiagonal s t a)}
{y : ↑(Set.mulAntidiagonal s t a)}
(h₁ : (↑x).fst ≤ (↑y).fst)
(h₂ : (↑x).snd ≤ (↑y).snd)
:
x = y
theorem
Set.AddAntidiagonal.finite_of_isPwo
{α : Type u_1}
[OrderedCancelAddCommMonoid α]
{s : Set α}
{t : Set α}
(hs : Set.IsPwo s)
(ht : Set.IsPwo t)
(a : α)
:
Set.Finite (Set.addAntidiagonal s t a)
theorem
Set.MulAntidiagonal.finite_of_isPwo
{α : Type u_1}
[OrderedCancelCommMonoid α]
{s : Set α}
{t : Set α}
(hs : Set.IsPwo s)
(ht : Set.IsPwo t)
(a : α)
:
Set.Finite (Set.mulAntidiagonal s t a)
theorem
Set.AddAntidiagonal.finite_of_isWf
{α : Type u_1}
[LinearOrderedCancelAddCommMonoid α]
{s : Set α}
{t : Set α}
(hs : Set.IsWf s)
(ht : Set.IsWf t)
(a : α)
:
Set.Finite (Set.addAntidiagonal s t a)
theorem
Set.MulAntidiagonal.finite_of_isWf
{α : Type u_1}
[LinearOrderedCancelCommMonoid α]
{s : Set α}
{t : Set α}
(hs : Set.IsWf s)
(ht : Set.IsWf t)
(a : α)
:
Set.Finite (Set.mulAntidiagonal s t a)