toCompletelyNormalSpace — Mathlib

English

A perfectly normal space is completely normal.

Русский

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

LaTeX

$$$ \operatorname{PerfectlyNormalSpace}(X) \Rightarrow \operatorname{CompletelyNormalSpace}(X) $$$

Lean4

instance (priority := 100) toCompletelyNormalSpace [PerfectlyNormalSpace X] : CompletelyNormalSpace X where
  completely_normal _ _ hd₁
    hd₂ :=
    separatedNhds_iff_disjoint.mp <|
      hasSeparatingCovers_iff_separatedNhds.mp
        ⟨(hd₂.hasSeparatingCover_closed_gdelta_right isClosed_closure <| closed_gdelta isClosed_closure).mono
            (fun ⦃_⦄ a ↦ a) subset_closure,
          ((Disjoint.symm hd₁).hasSeparatingCover_closed_gdelta_right isClosed_closure <|
                closed_gdelta isClosed_closure).mono
            (fun ⦃_⦄ a ↦ a) subset_closure⟩

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