mathlib documentation

data.set.pairwise

Relations holding pairwise #

This file defines pairwise relations.

Main declarations #

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

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

Equations
theorem set.pairwise_on_univ {α : Type u} {r : α → α → Prop} :
theorem set.pairwise_on.on_injective {α : Type u} {β : Type v} {s : set α} {r : α → α → Prop} (hs : s.pairwise_on r) {f : β → α} (hf : function.injective f) (hfs : ∀ (x : β), f x s) :
pairwise (r on f)
theorem pairwise.mono {α : Type u} {p q : α → α → Prop} (hp : pairwise p) (h : ∀ ⦃i j : α⦄, p i jq i j) :
theorem pairwise_on_bool {α : Type u} {r : α → α → Prop} (hr : symmetric r) {a b : α} :
pairwise (r on λ (c : bool), cond c a b) r a b
theorem pairwise_disjoint_on_bool {α : Type u} [semilattice_inf_bot α] {a b : α} :
pairwise (disjoint on λ (c : bool), cond c a b) disjoint a b
theorem symmetric.pairwise_on {α : Type u} {β : Type v} [linear_order β] {r : α → α → Prop} (hr : symmetric r) (f : β → α) :
pairwise (r on f) ∀ (m n : β), m < nr (f m) (f n)
theorem pairwise_disjoint_on {α : Type u} {β : Type v} [semilattice_inf_bot α] [linear_order β] (f : β → α) :
pairwise (disjoint on f) ∀ (m n : β), m < ndisjoint (f m) (f n)
theorem pairwise.pairwise_on {α : Type u} {p : α → α → Prop} (h : pairwise p) (s : set α) :
theorem pairwise_disjoint_fiber {α : Type u} {β : Type v} (f : α → β) :
pairwise (disjoint on λ (y : β), f ⁻¹' {y})