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.pairwise_on
{α : Type u}
{p : α → α → Prop}
(h : pairwise p)
(s : set α) :
s.pairwise_on p
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.
theorem
set.disjoint_disjointed'
{α : Type u}
{f : ℕ → set α}
(i j : ℕ) :
i ≠ j → set.disjointed f i ∩ set.disjointed f j = ∅
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 t → p (t \ f i)) → p (set.disjointed f n)