instNormalSpace — Mathlib

English

The SeparationQuotient of a normal space is a normal space.

Русский

Фактор-пространство по сепарации нормального пространства также нормальное.

LaTeX

$$$ [NormalSpace X] \\Rightarrow [NormalSpace (SeparationQuotient X)]$$$

Lean4

/-- The `SeparationQuotient` of a normal space is a normal space. -/
instance [NormalSpace X] : NormalSpace (SeparationQuotient X) where
  normal s t hs ht
    hd :=
    separatedNhds_iff_disjoint.2 <|
      by
      rw [← disjoint_comap_iff surjective_mk, comap_mk_nhdsSet, comap_mk_nhdsSet]
      exact disjoint_nhdsSet_nhdsSet (hs.preimage continuous_mk) (ht.preimage continuous_mk) (hd.preimage mk)

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