English
There is a recursion principle for the disjointed construction: to define a property for disjointed f i, it suffices to define it for f n and extend through the successive subtractions.
Русский
Существование принципа рекурсии для построения disjointed: чтобы определить свойство для disjointed f i, достаточно определить его на f n и затем продолжать через последовательные вычитания.
LaTeX
$$$ \mathrm{disjointedRec} \{f: \mathbb{N} \to \alpha\} \{p: \alpha \to \mathrm{Sort}\} (hdiff) : \forall n, p(f(n)) \to p(\mathrm{disjointed} f n)$$$
Lean4
theorem disjointed_add_one [NoMaxOrder ι] (f : ι → α) (i : ι) : disjointed f (i + 1) = f (i + 1) \ partialSups f i := by
simpa only [succ_eq_add_one] using disjointed_succ f (not_isMax i)
