Relations holding pairwise

This file defines pairwise relations.

Main declarations

• Pairwise: Pairwise r states that r i j for all i ≠ j.
• Set.Pairwise: s.Pairwise r states that r i j for all i ≠ j with i, j ∈ s.

def Pairwise {α : Type u_1} (r : α → α → Prop) : Prop

A relation r holds pairwise if r i j for all i ≠ j.

Equations

• Pairwise r = ∀ ⦃i j : α⦄, i ≠ j → r i j

theorem Pairwise.mono {α : Type u_1} {r p : α → α → Prop} (hr : Pairwise r) (h : ∀ ⦃i j : α⦄, r i j → p i j) : Pairwise p

theorem Pairwise.eq {α : Type u_1} {r : α → α → Prop} {a b : α} (h : Pairwise r) : ¬r a b → a = b

@[simp]

theorem Subsingleton.pairwise {α : Type u_1} {r : α → α → Prop} [Subsingleton α] : Pairwise r

theorem Function.injective_iff_pairwise_ne {α : Type u_1} {ι : Type u_3} {f : ι → α} : Injective f ↔ Pairwise (onFun (fun (x1 x2 : α) => x1 ≠ x2) f)

theorem Function.Injective.pairwise_ne {α : Type u_1} {ι : Type u_3} {f : ι → α} : Injective f → Pairwise (onFun (fun (x1 x2 : α) => x1 ≠ x2) f)

Alias of the forward direction of Function.injective_iff_pairwise_ne.

theorem Pairwise.comp_of_injective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} (hr : Pairwise r) {f : β → α} (hf : Function.Injective f) : Pairwise (Function.onFun r f)

theorem Pairwise.of_comp_of_surjective {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {f : β → α} (hr : Pairwise (Function.onFun r f)) (hf : Function.Surjective f) : Pairwise r

theorem Function.Bijective.pairwise_comp_iff {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {f : β → α} (hf : Bijective f) : Pairwise (onFun r f) ↔ Pairwise r

theorem pairwise_fin_succ_iff {n : ℕ} {R : Fin n.succ → Fin n.succ → Prop} : Pairwise R ↔ (∀ (i : Fin n), R i.succ 0) ∧ (∀ (j : Fin n), R 0 j.succ) ∧ Pairwise fun (i j : Fin n) => R i.succ j.succ

theorem pairwise_fin_succ_iff_of_isSymm {n : ℕ} {R : Fin n.succ → Fin n.succ → Prop} [Std.Symm R] : Pairwise R ↔ (∀ (j : Fin n), R 0 j.succ) ∧ Pairwise fun (i j : Fin n) => R i.succ j.succ

def Set.Pairwise {α : Type u_1} (s : Set α) (r : α → α → Prop) : Prop

The relation r holds pairwise on the set s if r x y for all distinct x y ∈ s.

Equations

• s.Pairwise r = ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → r x y

theorem Set.pairwise_of_forall {α : Type u_1} (s : Set α) (r : α → α → Prop) (h : ∀ (a b : α), r a b) : s.Pairwise r

theorem Set.Pairwise.imp_on {α : Type u_1} {r p : α → α → Prop} {s : Set α} (h : s.Pairwise r) (hrp : s.Pairwise fun ⦃a b : α⦄ => r a b → p a b) : s.Pairwise p

theorem Set.Pairwise.imp {α : Type u_1} {r p : α → α → Prop} {s : Set α} (h : s.Pairwise r) (hpq : ∀ ⦃a b : α⦄, r a b → p a b) : s.Pairwise p

theorem Set.Pairwise.eq {α : Type u_1} {r : α → α → Prop} {s : Set α} {a b : α} (hs : s.Pairwise r) (ha : a ∈ s) (hb : b ∈ s) (h : ¬r a b) : a = b

theorem Set.pairwise_iff_of_refl {α : Type u_1} {r : α → α → Prop} {s : Set α} [Std.Refl r] : s.Pairwise r ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → r a b

theorem Set.Pairwise.forall₂ {α : Type u_1} {r : α → α → Prop} {s : Set α} [Std.Refl r] : s.Pairwise r → ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → r a b

Alias of the forward direction of Set.pairwise_iff_of_refl.

theorem Set.Pairwise.of_forall₂ {α : Type u_1} {r : α → α → Prop} {s : Set α} (h : ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → r a b) : s.Pairwise r

@[deprecated Set.Pairwise.forall₂ (since := "2026-08-14")]

theorem Set.Pairwise.of_refl {α : Type u_1} {r : α → α → Prop} {s : Set α} [Std.Refl r] : s.Pairwise r → ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → r a b

Alias of Set.Pairwise.forall₂.

---

Alias of the forward direction of Set.pairwise_iff_of_refl.

@[deprecated Set.pairwise_iff_of_refl (since := "2026-08-14")]

theorem Std.Refl.set_pairwise_iff {α : Type u_1} {r : α → α → Prop} {s : Set α} [Refl r] : s.Pairwise r ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → r a b

Alias of Set.pairwise_iff_of_refl.

theorem Set.Pairwise.on_injective {α : Type u_1} {ι : Type u_3} {r : α → α → Prop} {f : ι → α} {s : Set α} (hs : s.Pairwise r) (hf : Function.Injective f) (hfs : ∀ (x : ι), f x ∈ s) : Pairwise (Function.onFun r f)

theorem Pairwise.set_pairwise {α : Type u_1} {r : α → α → Prop} (h : Pairwise r) (s : Set α) : s.Pairwise r