English
If f is an IsNormal function, then for every o and every g with a domain a < o, applying f to the bsup over o equals the bsup over o of the function applying f to g; that is, f(bsup o g) = bsup o (λ a h, f(g a h)).
Русский
Если f нормальная функция, то для любого o и любого g верно: f(выборка bsup по o) = bsup по o от функции, применяющей f к g.
LaTeX
$$$f \\text{ is normal } \\Rightarrow \\forall o\\, \\forall g : \\forall a < o, \\operatorname{Ordinal},\\; f(\\operatorname{bsup}(o, g)) = \\operatorname{bsup}(o, (\\lambda a\\, h. f(g(a,h))))$$$
Lean4
theorem bsup {f : Ordinal → Ordinal} (H : IsNormal f) {o : Ordinal} :
∀ (g : ∀ a < o, Ordinal), o ≠ 0 → f (bsup o g) = bsup o fun a h => f (g a h) :=
inductionOn o fun α r _ g h => by
haveI := type_ne_zero_iff_nonempty.1 h
rw [← iSup'_eq_bsup r, IsNormal.map_iSup H, ← iSup'_eq_bsup r] <;> rfl
