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.