English
In an infinite discrete space X, the inverse of the cofinite topology on the OnePoint compactification is not continuous.
Русский
Для бесконечного дискретного пространства X обратная когнатыя (кофинитная топология) на одномточечном компакт-компактировании не непрерывна.
LaTeX
$$$ \\neg \\text{Continuous}((\\operatorname{CofiniteTopology.of (OnePoint X)}).symm)$$$
Lean4
/-- If `X` is an infinite type with discrete topology (e.g., `ℕ`), then the identity map from
`CofiniteTopology (OnePoint X)` to `OnePoint X` is not continuous. -/
theorem not_continuous_cofiniteTopology_of_symm [Infinite X] [DiscreteTopology X] :
¬Continuous (@CofiniteTopology.of (OnePoint X)).symm :=
by
inhabit X
simp only [continuous_iff_continuousAt, ContinuousAt, not_forall]
use CofiniteTopology.of ↑(default : X)
simpa [nhds_coe_eq, nhds_discrete, CofiniteTopology.nhds_eq] using
(finite_singleton ((default : X) : OnePoint X)).infinite_compl
