English
If f is monotone on succ o, then the bsup over succ o equals the value at o with the index proof lt_succ(o).
Русский
Если f монотонна на окрестности succ o, то bsup над succ o равен значению при аргументе o с доказательством lt_succ(o).
LaTeX
$$$\\forall o\\, \\forall f, (\\forall i j, (hi : i < \\operatorname{succ}(o)) (hj : j < \\operatorname{succ}(o)), i \\le j \\rightarrow f(i, hi) \\le f(j, hj)) \\Rightarrow \\operatorname{bsup}(succ(o), f) = f(o, \\text{lt\_succ}(o))$$$
Lean4
theorem bsup_succ_of_mono {o : Ordinal} {f : ∀ a < succ o, Ordinal} (hf : ∀ {i j} (hi hj), i ≤ j → f i hi ≤ f j hj) :
bsup _ f = f o (lt_succ o) :=
le_antisymm (bsup_le fun _i hi => hf _ _ <| le_of_lt_succ hi) (le_bsup _ _ _)
