English
Let α and β be well-ordered topological spaces (with the order topology). If f: α → β is normal, then f is continuous.
Русский
Пусть α и β — хорошо упорядоченные топологические пространства с порядковой топологией. Если f: α → β нормальная функция, то она непрерывна.
LaTeX
$$$\\text{IsNormal}(f) \\Rightarrow \\text{Continuous}(f)$$$
Lean4
theorem continuous {f : α → β} (hf : IsNormal f) : Continuous f :=
by
rw [OrderTopology.continuous_iff]
refine fun b ↦ ⟨?_, ((isLowerSet_Iio b).preimage hf.strictMono.monotone).isOpen⟩
rw [← isClosed_compl_iff, ← Set.preimage_compl, Set.compl_Ioi]
obtain ha | ⟨a, ha⟩ := ((isLowerSet_Iic b).preimage hf.strictMono.monotone).eq_univ_or_Iio
· exact ha ▸ isClosed_univ
· obtain h | h := (f ⁻¹' Iic b).eq_empty_or_nonempty
· exact h ▸ isClosed_empty
· have : Nonempty α := ⟨a⟩
have : Nonempty β := ⟨b⟩
rw [hf.preimage_Iic h (ha ▸ bddAbove_Iio)]
exact isClosed_Iic
