English
IsNormal f iff (i) for all a, f(a) < f(a+1) and (ii) for every succ-limit o, bsup o fun x => f x equals f o.
Русский
IsNormal f эквивалентно (i) для всех a: f(a) < f(a+1) и (ii) для каждого o, являющегося пределом-сукцессии, bsup o f = f(o).
LaTeX
$$$ \\text{IsNormal}(f) \\iff (\\forall a, f(a) < f(\\operatorname{succ}(a))) \\land \\forall o, \\text{IsSuccLimit}(o) \\Rightarrow (\\operatorname{bsup}(o, f) = f(o)) $$$
Lean4
theorem isNormal_iff_lt_succ_and_bsup_eq {f : Ordinal.{u} → Ordinal.{max u v}} :
IsNormal f ↔ (∀ a, f a < f (succ a)) ∧ ∀ o, IsSuccLimit o → (bsup.{_, v} o fun x _ => f x) = f o :=
⟨fun h => ⟨fun a ↦ h.strictMono (lt_succ a), @IsNormal.bsup_eq f h⟩, fun ⟨h₁, h₂⟩ =>
.of_succ_lt h₁ fun ho ↦ by
rw [← h₂ _ ho]
simpa [IsLUB, upperBounds, lowerBounds, IsLeast, bsup_le_iff] using le_bsup _⟩
