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) :
theorem
pairwise.mono
{α : Type u}
{p q : α → α → Prop}
(h : ∀ ⦃i j : α⦄, p i j → q i j)
(hp : pairwise p) :
pairwise q
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.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}
(h₁ : p (f n))
(h₂ : ∀ (t : set α) (i : ℕ), p t → p (t \ f i)) :
p (set.disjointed f n)