# mathlibdocumentation

data.set.disjointed

# Relations holding pairwise and consecutive differences of sets #

This file defines pairwise relations and a way to make a sequence of sets into a sequence of disjoint sets.

## Main declarations #

• pairwise p: States that p i j for all i ≠ j.
• disjointed f: Yields the sequence of sets f 0, f 1 \ f 0, f 2 \ (f 0 ∪ f 1), ... This sequence has the same union as f 0, f 1, f 2 but with disjoint sets.
def pairwise {α : Type u_1} (p : α → α → Prop) :
Prop

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

Equations
• = ∀ (i j : α), i jp i j
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} (h : ∀ ⦃i j : α⦄, p i jq i j) (hp : pairwise p) :
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} {a b : α} :
pairwise (disjoint on λ (c : bool), cond c a b) b
theorem pairwise_on_nat {α : Type u} {r : α → α → Prop} (hr : symmetric r) (f : → α) :
pairwise (r on f) ∀ (m n : ), m < nr (f m) (f n)
theorem pairwise_disjoint_on_nat {α : Type u} (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})
def set.disjointed {α : Type u} (f : set α) (n : ) :
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 : ) :
i j =
theorem set.disjointed_subset {α : Type u} {f : set α} {n : } :
f 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.disjointed_induct {α : Type u} {f : set α} {n : } {p : set α → Prop} (h₁ : p (f n)) (h₂ : ∀ (t : set α) (i : ), p tp (t \ f i)) :
p n)
theorem set.disjointed_of_mono {α : Type u} {f : set α} {n : } (hf : monotone f) :
(n + 1) = f (n + 1) \ f n
theorem set.subset_Union_disjointed {α : Type u} {f : set α} {n : } :
f n ⋃ (i : ) (H : i < n.succ),
theorem set.Union_disjointed {α : Type u} {f : set α} :
(⋃ (n : ), n) = ⋃ (n : ), f n
theorem set.Union_disjointed_of_mono {α : Type u} {f : set α} (hf : monotone f) (n : ) :
(⋃ (i : ) (H : i < n.succ), i) = f n