Multiplication antidiagonal

def Set.mulAntidiagonal {α : Type u_1} [Mul α] (s 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.antidiagonal {α : Type u_1} [Add α] (s 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.antidiagonal t a = {x : α × α | x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 + x.2 = a}

@[simp]

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

@[simp]

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

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

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

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

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

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

theorem Set.swap_mem_antidiagonal {α : Type u_1} [AddCommMagma α] {s t : Set α} {a : α} {x : α × α} : x.swap ∈ s.antidiagonal t a ↔ x ∈ t.antidiagonal s a

@[simp]

theorem Set.swap_mem_mulAntidiagonal_aux {α : Type u_1} [CommMagma α] {s 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_antidiagonal_aux {α : Type u_1} [AddCommMagma α] {s t : Set α} {a : α} {x : α × α} : x.2 ∈ s ∧ x.1 ∈ t ∧ x.2 + x.1 = a ↔ x ∈ t.antidiagonal s a

theorem Set.MulAntidiagonal.fst_eq_fst_iff_snd_eq_snd {α : Type u_1} [CommMonoid α] [IsCancelMul α] {s t : Set α} {a : α} {x 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} [AddCommMonoid α] [IsCancelAdd α] {s t : Set α} {a : α} {x y : ↑(s.antidiagonal t a)} : (↑x).1 = (↑y).1 ↔ (↑x).2 = (↑y).2

theorem Set.MulAntidiagonal.eq_of_fst_eq_fst {α : Type u_1} [CommMonoid α] [IsCancelMul α] {s t : Set α} {a : α} {x y : ↑(s.mulAntidiagonal t a)} (h : (↑x).1 = (↑y).1) : x = y

theorem Set.AddAntidiagonal.eq_of_fst_eq_fst {α : Type u_1} [AddCommMonoid α] [IsCancelAdd α] {s t : Set α} {a : α} {x y : ↑(s.antidiagonal t a)} (h : (↑x).1 = (↑y).1) : x = y

theorem Set.MulAntidiagonal.eq_of_snd_eq_snd {α : Type u_1} [CommMonoid α] [IsCancelMul α] {s t : Set α} {a : α} {x y : ↑(s.mulAntidiagonal t a)} (h : (↑x).2 = (↑y).2) : x = y

theorem Set.AddAntidiagonal.eq_of_snd_eq_snd {α : Type u_1} [AddCommMonoid α] [IsCancelAdd α] {s t : Set α} {a : α} {x y : ↑(s.antidiagonal t a)} (h : (↑x).2 = (↑y).2) : x = y

theorem Set.MulAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsCancelMul α] [MulLeftMono α] [MulRightStrictMono α] (s t : Set α) (a : α) {x 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} [AddCommMonoid α] [PartialOrder α] [IsCancelAdd α] [AddLeftMono α] [AddRightStrictMono α] (s t : Set α) (a : α) {x y : ↑(s.antidiagonal t a)} (h₁ : (↑x).1 ≤ (↑y).1) (h₂ : (↑x).2 ≤ (↑y).2) : x = y

theorem Set.MulAntidiagonal.finite_of_isPWO {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsCancelMul α] [MulLeftMono α] [MulRightStrictMono α] {s t : Set α} (hs : s.IsPWO) (ht : t.IsPWO) (a : α) : (s.mulAntidiagonal t a).Finite

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

theorem Set.MulAntidiagonal.finite_of_isWF {α : Type u_1} [CancelCommMonoid α] [LinearOrder α] [MulLeftMono α] [MulRightStrictMono α] {s 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 t : Set α} (hs : s.IsWF) (ht : t.IsWF) (a : α) : (s.antidiagonal t a).Finite