English
Let o be an ordinal and f assign to each a < o an ordinal. Then for any a, a is below the supremum of f over a iff some indexed value of f is above a; i.e. a < bsup(o, f) if and only if there exists i with hi : i < o and a < f(i, hi).
Русский
Пусть o — ординал и для каждого a < o задан ординал f(a). Тогда имеет место: a меньше наибольшего элемента семейства f ⇔ существует индекс i с доказательством hi: i < o и a < f(i, hi).
LaTeX
$$$a < \\operatorname{bsup}(o, f) \\iff \\exists i\\, (hi : i < o) \\wedge a < f(i, hi)$$$
Lean4
theorem lt_bsup {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) {a} : a < bsup.{_, v} o f ↔ ∃ i hi, a < f i hi := by
simpa only [not_forall, not_le] using not_congr (@bsup_le_iff.{_, v} _ f a)
