English
Let f : ι → α and i ∈ ι with i not maximal. Then disjointed f at the successor of i equals f at the successor of i minus the partial sups up to i: disjointed f (succ i) = f (succ i) \ partialSups f i.
Русский
Пусть f : ι → α и i ∈ ι так, что i не максимум. Тогда disjointed f на successor(i) равен f на successor(i) минус частичные верхние пределы до i: disjointed f (succ i) = f (succ i) \ partialSups f i.
LaTeX
$$$\forall f : ι \to α\quad \forall i : ι,\; \neg\operatorname{IsMax}(i) \Rightarrow \operatorname{disjointed} f (\operatorname{succ} i) = f(\operatorname{succ} i) \setminus \partialSups f i$$$
Lean4
theorem disjointed_succ (f : ι → α) {i : ι} (hi : ¬IsMax i) : disjointed f (succ i) = f (succ i) \ partialSups f i :=
by
rw [disjointed_apply, partialSups_apply, sup'_eq_sup]
congr 2 with m
simpa only [mem_Iio, mem_Iic] using lt_succ_iff_of_not_isMax hi
