English
For a function f from ordinals to ordinals, IsNormal f holds if and only if f is strictly monotone and satisfies a limit condition: for every o that is a succ-limit, for every a, if f(b) ≤ a holds for all b < o, then f(o) ≤ a.
Русский
Для функции f : Ordinal → Ordinal справедливо IsNormal f тогда и только тогда, когда f строго возрастает и удовлетворяет предел-условию: для каждого o, являющегося succ-пределом, для каждого a, если f(b) ≤ a для всех b < o, то f(o) ≤ a.
LaTeX
$$$\mathrm{IsNormal}(f) \iff \Big(\mathrm{StrictMono}(f) \ \land\ \forall o, \mathrm{IsSuccLimit}(o) \to \forall a, (\forall b < o, f(b) \le a) \to f(o) \le a\Big).$$$
Lean4
theorem isNormal_iff_strictMono_limit (f : Ordinal → Ordinal) :
IsNormal f ↔ StrictMono f ∧ ∀ o, IsSuccLimit o → ∀ a, (∀ b < o, f b ≤ a) → f o ≤ a :=
isNormal_iff
