instPerfectlyNormalSpaceOfPseudoMetrizableSpace

English

A perfectly normal space X holds when X is pseudo-metrizable.

Русский

Полностью нормальное пространство возникает для псевдометризируемого пространства.

LaTeX

$$instPerfectlyNormalSpaceOfPseudoMetrizableSpace : [TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] ⇒ PerfectlyNormalSpace X$$

Lean4

instance (priority := 500) [PseudoMetrizableSpace X] : PerfectlyNormalSpace X where
  closed_gdelta s
    hs := by
    let _ := pseudoMetrizableSpacePseudoMetric X
    rcases (@uniformity_hasBasis_open X _).exists_antitone_subbasis with ⟨U, hUo, hU, -⟩
    rw [← hs.closure_eq, ← hU.biInter_biUnion_ball]
    refine .biInter (to_countable _) fun n _ => IsOpen.isGδ ?_
    exact isOpen_biUnion fun x _ => UniformSpace.isOpen_ball _ (hUo _).2

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