# 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 sequence`f 0`

,`f 1 \ f 0`

,`f 2 \ (f 0 ⊔ 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`

.`iSup_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 0 = f 0
- disjointed f n.succ = f (n + 1) \ (partialSups f) n

## 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.

## Equations

- disjointedRec hdiff = id
- disjointedRec hdiff = fun (h : p (f (n + 1))) => let_fun H := fun (k : ℕ) => Nat.recAux (hdiff h) (fun (k : ℕ) (ih : p (f (n + 1) \ (partialSups f) k)) => ⋯.mpr (⋯.mpr (hdiff ih))) k; H n

## Instances For

`disjointed f`

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

.