Multiplication antidiagonal

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

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

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

• Set.mulAntidiagonal s t a = {x | 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 ∈ Set.addAntidiagonal s t a ↔ 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 ∈ Set.mulAntidiagonal s t a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 * x.2 = a

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

@[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 ∈ Set.addAntidiagonal t 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 ∈ 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)} : (↑x).1 = (↑y).1 ↔ (↑x).2 = (↑y).2

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

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).1 = (↑y).1) : 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).1 = (↑y).1) : 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).2 = (↑y).2) : 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).2 = (↑y).2) : 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).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} [OrderedCancelCommMonoid α] (s : Set α) (t : Set α) (a : α) {x : ↑(Set.mulAntidiagonal s t a)} {y : ↑(Set.mulAntidiagonal s t a)} (h₁ : (↑x).1 ≤ (↑y).1) (h₂ : (↑x).2 ≤ (↑y).2) : 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)