Consecutive differences of sets #
This file defines the way to make a sequence of elements into a sequence of disjoint elements with the same partial sups.
For a sequence
f : ℕ → α, this new sequence will be
f 1 \ f 0,
f 2 \ (f 0 ⊔ f 1).
It is actually unique, as
Main declarations #
disjointed f: The sequence
f 1 \ f 0,
f 2 \ (f 0 ⊔ f 1), ....
disjointed fhas the same partial sups as
disjoint_disjointed: The elements of
disjointed fare pairwise disjoint.
disjointed fis the only pairwise disjoint sequence having the same partial sups as
disjointed fhas the same supremum as
f. Limiting case of
We also provide set notation variants of some lemmas.
Find a useful statement of
One could generalize
disjointed to any locally finite bot preorder domain, in place of
Related to the TODO in the module docstring of
f : ℕ → α is a sequence of elements, then
disjointed f is the sequence formed by
subtracting each element from the nexts. This is the unique disjoint sequence whose partial sups
are the same as the original sequence.
- disjointed f (n + 1) = f (n + 1) \ ⇑(partial_sups f) n
- disjointed f 0 = f 0
An induction principle for
disjointed. To define/prove something on
disjointed f n, it's
enough to define/prove it for
f n and being able to extend through diffs.
- disjointed_rec hdiff = λ (h : p (f (n + 1))), (λ (k : ℕ), nat.rec (hdiff h) (λ (k : ℕ) (ih : p (f (n + 1) \ ⇑(partial_sups f) k)), _.mpr (_.mpr (hdiff ih))) k) n
- disjointed_rec hdiff = id
disjointed f is the unique sequence that is pairwise disjoint and has the same partial sups