of_regularSpace_lindelofSpace — Mathlib

English

A regular space X with a Lindelöf topology is a normal space.

Русский

Регулярное пространство X с линдёловой топологией нормальное.

LaTeX

$$$ [RegularSpace X] \\land [LindelofSpace X] \\Rightarrow \\ NormalSpace X $$$

Lean4

/-- A regular topological space with a Lindelöf topology is a normal space. A consequence of e.g.
Corollaries 20.8 and 20.10 of [Willard's *General Topology*][zbMATH02107988] (without the
assumption of Hausdorff). -/
instance (priority := 100) of_regularSpace_lindelofSpace [RegularSpace X] [LindelofSpace X] : NormalSpace X where
  normal _ _ hcl kcl
    hkdis :=
    hasSeparatingCovers_iff_separatedNhds.mp
      ⟨hcl.HasSeparatingCover kcl hkdis, kcl.HasSeparatingCover hcl (Disjoint.symm hkdis)⟩

Похожие утверждения