bsup_eq — Mathlib

English

If f is an IsNormal function, then bsup over o with f equals f at o, provided o is a succ-limit ordinal.

Русский

Если f нормальная функция, то bsup над o с f равен f(o), если o — предел-сукцессия.

LaTeX

$$$ \\text{IsNormal}(f) \\Rightarrow \\forall o,\\ IsSuccLimit(o) \\Rightarrow (\\operatorname{bsup}(o, f) = f(o)) $$$

Lean4

theorem bsup_eq {f : Ordinal.{u} → Ordinal.{max u v}} (H : IsNormal f) {o : Ordinal.{u}} (h : IsSuccLimit o) :
    (Ordinal.bsup.{_, v} o fun x _ => f x) = f o := by
  rw [← IsNormal.bsup.{u, u, v} H (fun x _ => x) h.ne_bot, bsup_id_limit fun _ ↦ h.succ_lt]

Похожие утверждения