English
There exists a concrete counterexample showing that a certain generalization fails: there is a compact space α=OnePoint ℕ and a cofinite topology β=OnePoint ℕ with identity map α→β continuous but not a homeomorphism.
Русский
Существует конкретный контрпример, показывающий, что общая идея неверна: есть компактное пространство α=OnePoint ℕ и когомпактная топология β=OnePoint ℕ, для которых тождественное отображение α→β непрерывно, но не является гомеоморфизмом.
LaTeX
$$$\\exists \\alpha,\\beta, f: \\alpha \\to \\beta$ такие что $\\alpha$ компактно, $\\beta$ T1, $f$ непрерывно, но $f^{-1}$ не непрерывно.$$
Lean4
/-- A concrete counterexample shows that `Continuous.homeoOfEquivCompactToT2`
cannot be generalized from `T2Space` to `T1Space`.
Let `α = OnePoint ℕ` be the one-point compactification of `ℕ`, and let `β` be the same space
`OnePoint ℕ` with the cofinite topology. Then `α` is compact, `β` is T1, and the identity map
`id : α → β` is a continuous equivalence that is not a homeomorphism.
-/
theorem t1_counterexample :
∃ (α β : Type) (_ : TopologicalSpace α) (_ : TopologicalSpace β),
CompactSpace α ∧ T1Space β ∧ ∃ f : α ≃ β, Continuous f ∧ ¬Continuous f.symm :=
⟨OnePoint ℕ, CofiniteTopology (OnePoint ℕ), inferInstance, inferInstance, inferInstance, inferInstance,
CofiniteTopology.of, CofiniteTopology.continuous_of, OnePoint.not_continuous_cofiniteTopology_of_symm⟩
