blsub_eq — Mathlib

English

For any IsNormal f and succ-limit o, blsub o f equals f o.

Русский

Для любой IsNormal f и предела-сукцессии o, равенство blsub o f = f(o).

LaTeX

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

Lean4

theorem blsub_eq {f : Ordinal.{u} → Ordinal.{max u v}} (H : IsNormal f) {o : Ordinal.{u}} (h : IsSuccLimit o) :
    (blsub.{_, v} o fun x _ => f x) = f o :=
  by
  rw [← IsNormal.bsup_eq.{u, v} H h, bsup_eq_blsub_of_lt_succ_limit h]
  exact fun a _ => H.strictMono (lt_succ a)

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