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 jfor all
i ≠ j.
disjointed f: Yields the sequence of sets
f 1 \ f 0,
f 2 \ (f 0 ∪ f 1), ... This sequence has the same union as
f 2but with disjoint sets.
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.