Multiplication antidiagonal

def Set.mulAntidiagonal {α : Type u_1} [Mul α] (s : Set α) (t : Set α) (a : α) : Set (α × α)

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.

Equations

• s.mulAntidiagonal t a = {x : α × α | x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 * x.2 = a}

def Set.addAntidiagonal {α : Type u_1} [Add α] (s : Set α) (t : Set α) (a : α) : Set (α × α)

Set.addAntidiagonal s t a is the set of all pairs of an element in s and an element in t that add to a.

Equations

• s.addAntidiagonal t a = {x : α × α | x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 + x.2 = a}

@[simp]

theorem Set.mem_mulAntidiagonal {α : Type u_1} [Mul α] {s : Set α} {t : Set α} {a : α} {x : α × α} : x ∈ s.mulAntidiagonal t a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 * x.2 = a

@[simp]

theorem Set.mem_addAntidiagonal {α : Type u_1} [Add α] {s : Set α} {t : Set α} {a : α} {x : α × α} : x ∈ s.addAntidiagonal t a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 + x.2 = a

theorem Set.mulAntidiagonal_mono_left {α : Type u_1} [Mul α] {s₁ : Set α} {s₂ : Set α} {t : Set α} {a : α} (h : s₁ ⊆ s₂) : s₁.mulAntidiagonal t a ⊆ s₂.mulAntidiagonal t a

theorem Set.addAntidiagonal_mono_left {α : Type u_1} [Add α] {s₁ : Set α} {s₂ : Set α} {t : Set α} {a : α} (h : s₁ ⊆ s₂) : s₁.addAntidiagonal t a ⊆ s₂.addAntidiagonal t a

theorem Set.mulAntidiagonal_mono_right {α : Type u_1} [Mul α] {s : Set α} {t₁ : Set α} {t₂ : Set α} {a : α} (h : t₁ ⊆ t₂) : s.mulAntidiagonal t₁ a ⊆ s.mulAntidiagonal t₂ a

theorem Set.addAntidiagonal_mono_right {α : Type u_1} [Add α] {s : Set α} {t₁ : Set α} {t₂ : Set α} {a : α} (h : t₁ ⊆ t₂) : s.addAntidiagonal t₁ a ⊆ s.addAntidiagonal t₂ a

theorem Set.swap_mem_mulAntidiagonal {α : Type u_1} [CommSemigroup α] {s : Set α} {t : Set α} {a : α} {x : α × α} : x.swap ∈ s.mulAntidiagonal t a ↔ x ∈ t.mulAntidiagonal s a

theorem Set.swap_mem_addAntidiagonal {α : Type u_1} [AddCommSemigroup α] {s : Set α} {t : Set α} {a : α} {x : α × α} : x.swap ∈ s.addAntidiagonal t a ↔ x ∈ t.addAntidiagonal s a

@[simp]

theorem Set.swap_mem_mulAntidiagonal_aux {α : Type u_1} [CommSemigroup α] {s : Set α} {t : Set α} {a : α} {x : α × α} : x.2 ∈ s ∧ x.1 ∈ t ∧ x.2 * x.1 = a ↔ x ∈ t.mulAntidiagonal s a

@[simp]

theorem Set.swap_mem_addAntidiagonal_aux {α : Type u_1} [AddCommSemigroup α] {s : Set α} {t : Set α} {a : α} {x : α × α} : x.2 ∈ s ∧ x.1 ∈ t ∧ x.2 + x.1 = a ↔ x ∈ t.addAntidiagonal s 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)} : (↑x).1 = (↑y).1 ↔ (↑x).2 = (↑y).2

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)} : (↑x).1 = (↑y).1 ↔ (↑x).2 = (↑y).2

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_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_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_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_fst_le_fst_of_snd_le_snd {α : Type u_1} [CancelCommMonoid α] [PartialOrder α] [MulLeftMono α] [MulRightStrictMono α] (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.eq_of_fst_le_fst_of_snd_le_snd {α : Type u_1} [AddCancelCommMonoid α] [PartialOrder α] [AddLeftMono α] [AddRightStrictMono α] (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.finite_of_isPWO {α : Type u_1} [CancelCommMonoid α] [PartialOrder α] [MulLeftMono α] [MulRightStrictMono α] {s : Set α} {t : Set α} (hs : s.IsPWO) (ht : t.IsPWO) (a : α) : (s.mulAntidiagonal t a).Finite

theorem Set.AddAntidiagonal.finite_of_isPWO {α : Type u_1} [AddCancelCommMonoid α] [PartialOrder α] [AddLeftMono α] [AddRightStrictMono α] {s : Set α} {t : Set α} (hs : s.IsPWO) (ht : t.IsPWO) (a : α) : (s.addAntidiagonal t a).Finite

theorem Set.MulAntidiagonal.finite_of_isWF {α : Type u_1} [CancelCommMonoid α] [LinearOrder α] [MulLeftMono α] [MulRightStrictMono α] {s : Set α} {t : Set α} (hs : s.IsWF) (ht : t.IsWF) (a : α) : (s.mulAntidiagonal t a).Finite

theorem Set.AddAntidiagonal.finite_of_isWF {α : Type u_1} [AddCancelCommMonoid α] [LinearOrder α] [AddLeftMono α] [AddRightStrictMono α] {s : Set α} {t : Set α} (hs : s.IsWF) (ht : t.IsWF) (a : α) : (s.addAntidiagonal t a).Finite