English
The inequality succ(bsup o f) ≤ blsub o f holds precisely when there exists i < o with f(i, hi) = bsup o f.
Русский
Неравенство succ(bsup o f) ≤ blsub o f эквивалентно существованию i < o такого, что f(i, hi) = bsup o f.
LaTeX
$$$ \\operatorname{succ}(\\operatorname{bsup}(o,f)) \\le \\operatorname{blsub}(o,f) \\iff \\exists i\\, \\exists hi, f(i,hi) = \\operatorname{bsup}(o,f) $$$
Lean4
theorem bsup_succ_le_blsub {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) :
succ (bsup.{_, v} o f) ≤ blsub.{_, v} o f ↔ ∃ i hi, f i hi = bsup.{_, v} o f :=
by
refine ⟨fun h => ?_, ?_⟩
· by_contra! hf
exact ne_of_lt (succ_le_iff.1 h) (le_antisymm (bsup_le_blsub f) (blsub_le (lt_bsup_of_ne_bsup.1 hf)))
rintro ⟨_, _, hf⟩
rw [succ_le_iff, ← hf]
exact lt_blsub _ _ _
