# 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) :

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

Equations
• = ∀ ⦃i j : α⦄, i jr i j
Instances For
theorem Pairwise.mono {α : Type u_1} {r : ααProp} {p : ααProp} (hr : ) (h : ∀ ⦃i j : α⦄, r i jp i j) :
theorem Pairwise.eq {α : Type u_1} {r : ααProp} {a : α} {b : α} (h : ) :
¬r a ba = b
theorem Subsingleton.pairwise {α : Type u_1} {r : ααProp} [] :
theorem Function.injective_iff_pairwise_ne {α : Type u_1} {ι : Type u_4} {f : ια} :
Pairwise ((fun (x1 x2 : α) => x1 x2) on f)
theorem Function.Injective.pairwise_ne {α : Type u_1} {ι : Type u_4} {f : ια} :
Pairwise ((fun (x1 x2 : α) => x1 x2) on 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 : ) {f : βα} (hf : ) :
Pairwise (r on f)
theorem Pairwise.of_comp_of_surjective {α : Type u_1} {β : Type u_2} {r : ααProp} {f : βα} (hr : Pairwise (r on f)) (hf : ) :
theorem Function.Bijective.pairwise_comp_iff {α : Type u_1} {β : Type u_2} {r : ααProp} {f : βα} (hf : ) :
Pairwise (r on f)
def Set.Pairwise {α : Type u_1} (s : Set α) (r : αα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 sx yr x y
Instances For
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 : ααProp} {p : ααProp} {s : Set α} (h : s.Pairwise r) (hrp : s.Pairwise fun ⦃a b : α⦄ => r a bp a b) :
s.Pairwise p
theorem Set.Pairwise.imp {α : Type u_1} {r : ααProp} {p : ααProp} {s : Set α} (h : s.Pairwise r) (hpq : ∀ ⦃a b : α⦄, r a bp 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 Reflexive.set_pairwise_iff {α : Type u_1} {r : ααProp} {s : Set α} (hr : ) :
s.Pairwise r ∀ ⦃a : α⦄, a s∀ ⦃b : α⦄, b sr a b
theorem Set.Pairwise.on_injective {α : Type u_1} {ι : Type u_4} {r : ααProp} {f : ια} {s : Set α} (hs : s.Pairwise r) (hf : ) (hfs : ∀ (x : ι), f x s) :
Pairwise (r on f)
theorem Pairwise.set_pairwise {α : Type u_1} {r : ααProp} (h : ) (s : Set α) :
s.Pairwise r