Multiplication antidiagonal #
theorem
Set.swap_mem_addAntidiagonal
{α : Type u_1}
[AddCommSemigroup α]
{s : Set α}
{t : Set α}
{a : α}
{x : α × α}
:
theorem
Set.swap_mem_mulAntidiagonal
{α : Type u_1}
[CommSemigroup α]
{s : Set α}
{t : Set α}
{a : α}
{x : α × α}
:
theorem
Set.AddAntidiagonal.fst_eq_fst_iff_snd_eq_snd
{α : Type u_1}
[AddCancelCommMonoid α]
{s : Set α}
{t : Set α}
{a : α}
{x : ↑(s.addAntidiagonal t a)}
{y : ↑(s.addAntidiagonal t a)}
:
theorem
Set.MulAntidiagonal.fst_eq_fst_iff_snd_eq_snd
{α : Type u_1}
[CancelCommMonoid α]
{s : Set α}
{t : Set α}
{a : α}
{x : ↑(s.mulAntidiagonal t a)}
{y : ↑(s.mulAntidiagonal t a)}
:
theorem
Set.AddAntidiagonal.eq_of_fst_eq_fst
{α : Type u_1}
[AddCancelCommMonoid α]
{s : Set α}
{t : Set α}
{a : α}
{x : ↑(s.addAntidiagonal t a)}
{y : ↑(s.addAntidiagonal t a)}
(h : (↑x).1 = (↑y).1)
:
x = y
theorem
Set.MulAntidiagonal.eq_of_fst_eq_fst
{α : Type u_1}
[CancelCommMonoid α]
{s : Set α}
{t : Set α}
{a : α}
{x : ↑(s.mulAntidiagonal t a)}
{y : ↑(s.mulAntidiagonal t a)}
(h : (↑x).1 = (↑y).1)
:
x = y
theorem
Set.AddAntidiagonal.eq_of_snd_eq_snd
{α : Type u_1}
[AddCancelCommMonoid α]
{s : Set α}
{t : Set α}
{a : α}
{x : ↑(s.addAntidiagonal t a)}
{y : ↑(s.addAntidiagonal t a)}
(h : (↑x).2 = (↑y).2)
:
x = y
theorem
Set.MulAntidiagonal.eq_of_snd_eq_snd
{α : Type u_1}
[CancelCommMonoid α]
{s : Set α}
{t : Set α}
{a : α}
{x : ↑(s.mulAntidiagonal t a)}
{y : ↑(s.mulAntidiagonal t a)}
(h : (↑x).2 = (↑y).2)
:
x = y
theorem
Set.AddAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd
{α : Type u_1}
[AddCancelCommMonoid α]
[PartialOrder α]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
[CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2]
(s : Set α)
(t : Set α)
(a : α)
{x : ↑(s.addAntidiagonal t a)}
{y : ↑(s.addAntidiagonal t a)}
(h₁ : (↑x).1 ≤ (↑y).1)
(h₂ : (↑x).2 ≤ (↑y).2)
:
x = y
theorem
Set.MulAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd
{α : Type u_1}
[CancelCommMonoid α]
[PartialOrder α]
[CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2]
[CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2]
(s : Set α)
(t : Set α)
(a : α)
{x : ↑(s.mulAntidiagonal t a)}
{y : ↑(s.mulAntidiagonal t a)}
(h₁ : (↑x).1 ≤ (↑y).1)
(h₂ : (↑x).2 ≤ (↑y).2)
:
x = y
theorem
Set.AddAntidiagonal.finite_of_isPWO
{α : Type u_1}
[AddCancelCommMonoid α]
[PartialOrder α]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
[CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2]
{s : Set α}
{t : Set α}
(hs : s.IsPWO)
(ht : t.IsPWO)
(a : α)
:
(s.addAntidiagonal t a).Finite
theorem
Set.MulAntidiagonal.finite_of_isPWO
{α : Type u_1}
[CancelCommMonoid α]
[PartialOrder α]
[CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2]
[CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2]
{s : Set α}
{t : Set α}
(hs : s.IsPWO)
(ht : t.IsPWO)
(a : α)
:
(s.mulAntidiagonal t a).Finite
theorem
Set.AddAntidiagonal.finite_of_isWF
{α : Type u_1}
[AddCancelCommMonoid α]
[LinearOrder α]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
[CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2]
{s : Set α}
{t : Set α}
(hs : s.IsWF)
(ht : t.IsWF)
(a : α)
:
(s.addAntidiagonal t a).Finite
theorem
Set.MulAntidiagonal.finite_of_isWF
{α : Type u_1}
[CancelCommMonoid α]
[LinearOrder α]
[CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2]
[CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2]
{s : Set α}
{t : Set α}
(hs : s.IsWF)
(ht : t.IsWF)
(a : α)
:
(s.mulAntidiagonal t a).Finite