English
A metrizable space X is normal.
Русский
Метрифицируемое пространство является нормальным.
LaTeX
$$[Priority] [PseudoMetrizableSpace X] ⇒ NormalSpace X$$
Lean4
instance (priority := 100) [PseudoMetrizableSpace X] : NormalSpace X where
normal s t hs ht
hst := by
let _ := pseudoMetrizableSpacePseudoMetric X
by_cases hee : s = ∅ ∨ t = ∅
· obtain rfl | rfl := hee <;> simp
simp only [not_or, ← ne_eq, ← nonempty_iff_ne_empty] at hee
obtain ⟨hse, hte⟩ := hee
let g (p : X) := infDist p t - infDist p s
have hg : Continuous g := by fun_prop
refine
⟨g ⁻¹' (Ioi 0), g ⁻¹' (Iio 0), isOpen_Ioi.preimage hg, isOpen_Iio.preimage hg, fun x hx ↦ ?_, fun x hx ↦ ?_,
Ioi_disjoint_Iio_same.preimage g⟩
· simp [g, infDist_zero_of_mem hx, (ht.notMem_iff_infDist_pos hte).mp (hst.notMem_of_mem_left hx)]
· simp [g, infDist_zero_of_mem hx, (hs.notMem_iff_infDist_pos hse).mp (hst.notMem_of_mem_right hx)]
