instT3SpaceSeparationQuotientOfRegularSpace

English

The SeparationQuotient of a regular space is a T3Space.

Русский

Разделённый квантор сепарации разделяет регулярное пространство как T3.

LaTeX

$$$[RegularSpace X] \Rightarrow [T3Space (SeparationQuotient X)].$$$

Lean4

/-- The `SeparationQuotient` of a regular space is a T₃ space. -/
instance [RegularSpace X] : T3Space (SeparationQuotient X) where
  regular {s a} hs
    ha := by
    rcases surjective_mk a with ⟨a, rfl⟩
    rw [← disjoint_comap_iff surjective_mk, comap_mk_nhds_mk, comap_mk_nhdsSet]
    exact RegularSpace.regular (hs.preimage continuous_mk) ha

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