# 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`.

source
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

Instances For

source
theorem Pairwise.mono {α : Type u_1} {r p : α → α → Prop} (hr : Pairwise r) (h : ∀ ⦃i j : α⦄, r i j → p i j) :
Pairwise p
source
theorem Pairwise.eq {α : Type u_1} {r : α → α → Prop} {a b : α} (h : Pairwise r) :
¬r a b → a = b
source
@[simp]
theorem Subsingleton.pairwise {α : Type u_1} {r : α → α → Prop} [Subsingleton α] :
Pairwise r
source
theorem Function.injective_iff_pairwise_ne {α : Type u_1} {ι : Type u_3} {f : ι → α} :
Injective f ↔ Pairwise (onFun (fun (x1 x2 : α) => x1 ≠ x2) f)
source
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`.

source
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)
source
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
source
theorem Function.Bijective.pairwise_comp_iff {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {f : β → α} (hf : Bijective f) :
Pairwise (onFun r f) ↔ Pairwise r
source
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
source
theorem pairwise_fin_succ_iff_of_isSymm {n : ℕ} {R : Fin n.succ → Fin n.succ → Prop} [IsSymm (Fin n.succ) R] :
Pairwise R ↔ (∀ (j : Fin n), R 0 j.succ) ∧ Pairwise fun (i j : Fin n) => R i.succ j.succ
source
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

Instances For

source
theorem Set.pairwise_of_forall {α : Type u_1} (s : Set α) (r : α → α → Prop) (h : ∀ (a b : α), r a b) :
s.Pairwise r
source
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
source
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
source
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
source
theorem Reflexive.set_pairwise_iff {α : Type u_1} {r : α → α → Prop} {s : Set α} (hr : Reflexive r) :
s.Pairwise r ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → r a b
source
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)
source
theorem Pairwise.set_pairwise {α : Type u_1} {r : α → α → Prop} (h : Pairwise r) (s : Set α) :
s.Pairwise r