English
If f is monotone, then for any i with i not maximal, disjointed f at succ i equals f succ i minus f i: disjointed f (succ i) = f (succ i) \ f i.
Русский
Если f монотонно возрастает, то для любого i, не являющегося максимумом, disjointed f на succ i равен f succ i минус f i.
LaTeX
$$$\forall f : ι \to α,\; \operatorname{Monotone} f \Rightarrow \forall i:\ ι,\; \neg \operatorname{IsMax}(i) \Rightarrow \operatorname{disjointed} f (\operatorname{succ} i) = f(\operatorname{succ} i) \setminus f(i)$$$
Lean4
protected theorem disjointed_succ {f : ι → α} (hf : Monotone f) {i : ι} (hn : ¬IsMax i) :
disjointed f (succ i) = f (succ i) \ f i := by rwa [disjointed_succ, hf.partialSups_eq]
