isClosed_infty — Mathlib

English

In the one-point compactification of a topological space X, the singleton set {∞} is a closed subset of OnePoint X.

Русский

В одноточечной компактфикации пространства X множество {∞} замкнуто.

LaTeX

$$$\operatorname{IsClosed} (\{ \infty \} : \operatorname{Set}(\operatorname{OnePoint} X))$$$

Lean4

theorem isClosed_infty : IsClosed ({∞} : Set (OnePoint X)) :=
  by
  rw [← compl_range_coe, isClosed_compl_iff]
  exact isOpen_range_coe

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