English
If o is a limit ordinal and f is strictly increasing along the increasing chain inside o, and successors stay inside o, then every value f(i,h) sits below bsup o f.
Русский
Пусть o — предельный ординал, f возрастает по цепочке внутри o, и переход к следующему остаётся внутри o; тогда f(i,h) < bsup(o,f) для всех i<h.
LaTeX
$$$hf: \\forall {a a'} (ha : a < o) (ha' : a' < o), a < a' \\rightarrow f(a, ha) < f(a', ha') \\ \\\\ ho: \\forall a < o, \\operatorname{succ}(a) < o \\\\ (i,h): f(i,h) < \\operatorname{bsup}(o,f)$$$
Lean4
theorem lt_bsup_of_limit {o : Ordinal} {f : ∀ a < o, Ordinal}
(hf : ∀ {a a'} (ha : a < o) (ha' : a' < o), a < a' → f a ha < f a' ha') (ho : ∀ a < o, succ a < o) (i h) :
f i h < bsup o f :=
(hf _ _ <| lt_succ i).trans_le (le_bsup f (succ i) <| ho _ h)
