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 #

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

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

Equations
theorem pairwise.mono {α : Type u_1} {r p : α α Prop} (hr : pairwise r) (h : ⦃i j : α⦄, r i j p i j) :
@[protected]
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 : ι α} :
theorem function.injective.pairwise_ne {α : Type u_1} {ι : Type u_4} {f : ι α} :

Alias of the forward direction of function.injective_iff_pairwise_ne.

@[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
theorem set.pairwise_of_forall {α : Type u_1} (s : set α) (r : α α Prop) (h : (a b : α), r a b) :
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)) :
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) :
@[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
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
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)
theorem pairwise.set_pairwise {α : Type u_1} {r : α α Prop} (h : pairwise r) (s : set α) :