English
For any f : Ordinal → Ordinal and hb: Not (BddAbove s), the equality enumOrd s = f holds iff f is StrictMono and range f = s.
Русский
Для любой функции f: Ordinal → Ordinal верно: enumOrd s = f тогда и только тогда, когда f строго монотонна и область значений равна s.
LaTeX
$$$$ \\mathrm{enumOrd}(s) = f \\;\\iff\\; (StrictMono\\;f) \\wedge (\\mathrm{range}\;f = s) $$$$
Lean4
/-- A characterization of `enumOrd`: it is the unique strict monotonic function with range `s`. -/
theorem eq_enumOrd (f : Ordinal → Ordinal) (hs : ¬BddAbove s) : enumOrd s = f ↔ StrictMono f ∧ range f = s :=
by
constructor
· rintro rfl
exact ⟨enumOrd_strictMono hs, range_enumOrd hs⟩
· rintro ⟨h₁, h₂⟩
rwa [← (enumOrd_strictMono hs).range_inj h₁, range_enumOrd hs, eq_comm]
