English
If f is monotone, then for every i, disjointed f (succ i) joined with f i equals f (succ i): disjointed f (succ i) ⊔ f i = f (succ i).
Русский
Если f монотонно, то для каждого i сумма disjointed f(succ i) и f i равна f(succ i).
LaTeX
$$$\forall f : ι \to α\; (hf : \operatorname{Monotone} f)\; \forall i:\ ι,\; \operatorname{Eq}(\operatorname{disjointed} f (\operatorname{succ} i) \sqcup f(i), f(\operatorname{succ} i))$$$
Lean4
/-- Note this lemma does not require `¬IsMax i`, unlike `disjointed_succ`. -/
theorem disjointed_succ_sup {f : ι → α} (hf : Monotone f) (i : ι) : disjointed f (succ i) ⊔ f i = f (succ i) :=
by
by_cases h : IsMax i
· simpa only [succ_eq_iff_isMax.mpr h, sup_eq_right] using disjointed_le f i
· rw [disjointed_apply]
have : Iio (succ i) = Iic i := by
ext
simp only [mem_Iio, lt_succ_iff_eq_or_lt_of_not_isMax h, mem_Iic, le_iff_lt_or_eq, Or.comm]
rw [this, ← sup'_eq_sup nonempty_Iic, ← partialSups_apply, hf.partialSups_eq, sdiff_sup_cancel <| hf <| le_succ i]
