toNormalSpace — Mathlib

English

A completely normal space is a normal space.

Русский

Полностью нормальное пространство является нормальным.

LaTeX

$$$ [CompletelyNormalSpace X] \\Rightarrow [NormalSpace X] $$$

Lean4

/-- A completely normal space is a normal space. -/
instance (priority := 100) toNormalSpace [CompletelyNormalSpace X] : NormalSpace X where
  normal s t hs ht
    hd := separatedNhds_iff_disjoint.2 <| completely_normal (by rwa [hs.closure_eq]) (by rwa [ht.closure_eq])

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