instCompactSpace — Mathlib

English

For any space X, the one-point compactification OnePoint X is a compact space.

Русский

Для любого пространства X однопунктовая компактфикация OnePoint X является компактным пространством.

LaTeX

$$$\\mathrm{OnePoint}(X) \\text{ is compact.}$$$

Lean4

/-- For any topological space `X`, its one point compactification is a compact space. -/
instance : CompactSpace (OnePoint X) where
  isCompact_univ :=
    by
    have : Tendsto ((↑) : X → OnePoint X) (cocompact X) (𝓝 ∞) :=
      by
      rw [nhds_infty_eq]
      exact (tendsto_map.mono_left cocompact_le_coclosedCompact).mono_right le_sup_left
    rw [← insert_none_range_some X]
    exact this.isCompact_insert_range_of_cocompact continuous_coe

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