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 0
, f 1 \ f 0
, f 2 \ (f 0 ⊔ f 1)
.
It is actually unique, as disjointed_unique
shows.
Main declarations #
disjointed f
: The sequencef 0
,f 1 \ f 0
,f 2 \ (f 0 ⊔ f 1)
, ....partialSups_disjointed
:disjointed f
has the same partial sups asf
.disjoint_disjointed
: The elements ofdisjointed f
are pairwise disjoint.disjointed_unique
:disjointed f
is the only pairwise disjoint sequence having the same partial sups asf
.iSup_disjointed
:disjointed f
has the same supremum asf
. Limiting case ofpartialSups_disjointed
.
We also provide set notation variants of some lemmas.
TODO #
Find a useful statement of disjointedRec_succ
.
One could generalize disjointed
to any locally finite bot preorder domain, in place of ℕ
.
Related to the TODO in the module docstring of Mathlib.Order.PartialSups
.
If 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.
Instances For
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.
Instances For
disjointed f
is the unique sequence that is pairwise disjoint and has the same partial sups
as f
.