English
IsNormal f iff (i) f(a) < f(succ a) for all a and (ii) for every succ-limit o, blsub o (fun x => f x) equals f o.
Русский
IsNormal f эквивалентно (i) f(a) < f(succ a) для всех a и (ii) для каждого o, являющегося пределом-сукцессии, blsub o (f) = f(o).
LaTeX
$$$ \\text{IsNormal}(f) \\iff (\\forall a, f(a) < f(\\operatorname{succ}(a))) \\land \\forall o, \\operatorname{IsSuccLimit}(o) \\Rightarrow (\\operatorname{blsub}(o, f) = f(o)) $$$
Lean4
theorem isNormal_iff_lt_succ_and_blsub_eq {f : Ordinal.{u} → Ordinal.{max u v}} :
IsNormal f ↔ (∀ a, f a < f (succ a)) ∧ ∀ o, IsSuccLimit o → (blsub.{_, v} o fun x _ => f x) = f o :=
by
rw [isNormal_iff_lt_succ_and_bsup_eq.{u, v}, and_congr_right_iff]
intro h
constructor <;> intro H o ho <;> have := H o ho <;> rwa [← bsup_eq_blsub_of_lt_succ_limit ho fun a _ => h a] at *
