mathlib3 documentation

logic.pairwise

Relations holding pairwise #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines pairwise relations.

Main declarations #

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

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

Equations
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
@[protected]
theorem pairwise.eq {α : Type u_1} {r : α → α → Prop} {a b : α} (h : pairwise r) :
¬r a b → a = b
source
theorem function.injective_iff_pairwise_ne {α : Type u_1} {ι : Type u_4} {f : ι → α} :
function.injective f ↔ pairwise (ne on f)
source
theorem function.injective.pairwise_ne {α : Type u_1} {ι : Type u_4} {f : ι → α} :
function.injective f → pairwise (ne on f)

Alias of the forward direction of function.injective_iff_pairwise_ne.

source
@[protected]
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
Instances for set.pairwise
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 (λ ⦃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
@[protected]
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_4} {r : α → α → Prop} {f : ι → α} {s : set α} (hs : s.pairwise r) (hf : function.injective f) (hfs : ∀ (x : ι), f x ∈ s) :
pairwise (r on f)
source
theorem pairwise.set_pairwise {α : Type u_1} {r : α → α → Prop} (h : pairwise r) (s : set α) :
s.pairwise r