# 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)⊔ f 1)`

.
It is actually unique, as `disjointed_unique`

shows.

## Main declarations #

`disjointed f`

: The sequence`f 0`

,`f 1 \ f 0`

,`f 2 \ (f 0 ⊔ f 1)⊔ f 1)`

, ....`partialSups_disjointed`

:`disjointed f`

has the same partial sups as`f`

.`disjoint_disjointed`

: The elements of`disjointed f`

are pairwise disjoint.`disjointed_unique`

:`disjointed f`

is the only pairwise disjoint sequence having the same partial sups as`f`

.`supᵢ_disjointed`

:`disjointed f`

has the same supremum as`f`

. Limiting case of`partialSups_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.

## Equations

- disjointed f x = match x with | 0 => f 0 | Nat.succ n => f (n + 1) \ ↑(partialSups f) n

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.

## Equations

- One or more equations did not get rendered due to their size.

`disjointed f`

is the unique sequence that is pairwise disjoint and has the same partial sups
as `f`

.