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 #

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

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

s.pairwise r = ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → r x y

Instances for set.pairwise

pairwise.decidable

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