instT1Space — Mathlib

English

If X is a T1 space, then OnePoint X is a T1 space.

Русский

Если X является пространством T1, то OnePoint X также является пространством T1.

LaTeX

$$$\\text{T1}(X) \\Rightarrow \\text{T1}(\\mathrm{OnePoint}(X)).$$$

Lean4

/-- The one point compactification of a `T1Space` space is a `T1Space`. -/
instance [T1Space X] : T1Space (OnePoint X) where
  t1
    z := by
    induction z using OnePoint.rec
    · exact isClosed_infty
    · rw [← image_singleton, isClosed_image_coe]
      exact ⟨isClosed_singleton, isCompact_singleton⟩

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