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 : α → α → Prop} {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

theorem Function.injective_iff_pairwise_ne {α : Type u_1} {ι : Type u_4} {f : ι → α} : Function.Injective f ↔ Pairwise ((fun x x_1 => x ≠ x_1) on f)

theorem Function.Injective.pairwise_ne {α : Type u_1} {ι : Type u_4} {f : ι → α} : Function.Injective f → Pairwise ((fun x x_1 => x ≠ x_1) on f)

Alias of the forward direction of Function.injective_iff_pairwise_ne.

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

• Set.Pairwise s 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) : Set.Pairwise s r

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

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

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

theorem Reflexive.set_pairwise_iff {α : Type u_1} {r : α → α → Prop} {s : Set α} (hr : Reflexive r) : Set.Pairwise s r ↔ ⦃a : α⦄ → a ∈ s → ⦃b : α⦄ → b ∈ s → r a b

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

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