mathlib documentation

data.set.disjointed

def pairwise {α : Type u_1} :
(α → α → 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 : β → α} :
function.injective f(∀ (x : β), f x s)pairwise (r on f)

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 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})

def set.disjointed {α : Type u} :
(set α)set α

If f : ℕ → set α is a sequence of sets, then disjointed f is the sequence formed with each set subtracted from the later ones in the sequence, to form a disjoint sequence.

Equations
theorem set.disjoint_disjointed {α : Type u} {f : set α} :

theorem set.disjoint_disjointed' {α : Type u} {f : set α} (i j : ) :

theorem set.disjointed_subset {α : Type u} {f : set α} {n : } :

theorem set.Union_lt_succ {α : Type u} {f : set α} {n : } :
(⋃ (i : ) (H : i < n.succ), f i) = f n ⋃ (i : ) (H : i < n), f i

theorem set.Inter_lt_succ {α : Type u} {f : set α} {n : } :
(⋂ (i : ) (H : i < n.succ), f i) = f n ⋂ (i : ) (H : i < n), f i

theorem set.subset_Union_disjointed {α : Type u} {f : set α} {n : } :
f n ⋃ (i : ) (H : i < n.succ), set.disjointed f i

theorem set.Union_disjointed {α : Type u} {f : set α} :
(⋃ (n : ), set.disjointed f n) = ⋃ (n : ), f n

theorem set.disjointed_induct {α : Type u} {f : set α} {n : } {p : set α → Prop} :
p (f n)(∀ (t : set α) (i : ), p tp (t \ f i))p (set.disjointed f n)

theorem set.disjointed_of_mono {α : Type u} {f : set α} {n : } :
monotone fset.disjointed f (n + 1) = f (n + 1) \ f n

theorem set.Union_disjointed_of_mono {α : Type u} {f : set α} (hf : monotone f) (n : ) :
(⋃ (i : ) (H : i < n.succ), set.disjointed f i) = f n