English
For well-ordered spaces with the order topology, a function f is normal if and only if it is strictly monotone and continuous.
Русский
Для хорошо упорядоченных пространств с порядковой топологией функция f нормальна тогда и только тогда, когда она строго монотонна и непрерывна.
LaTeX
$$$\\text{IsNormal}(f) \\;\\Leftrightarrow\\; (\\text{StrictMono}(f) \\land \\text{Continuous}(f))$$$
Lean4
/-- A normal function between well-orders is equivalent to a strictly monotone,
continuous function. -/
theorem isNormal_iff_strictMono_and_continuous {f : α → β} : IsNormal f ↔ StrictMono f ∧ Continuous f
where
mp hf := ⟨hf.strictMono, hf.continuous⟩
mpr := by
rintro ⟨hs, hc⟩
refine ⟨hs, fun {a} ha ↦ (isLUB_of_mem_closure ?_ ?_).2⟩
· rintro _ ⟨b, hb, rfl⟩
exact (hs hb).le
· apply image_closure_subset_closure_image hc (mem_image_of_mem ..)
exact ha.isLUB_Iio.mem_closure (Iio_nonempty.2 ha.1)
