Theorems · Theorem · general topology

OnePoint.not_continuous_cofiniteTopology_of_symm

∀ {X : Type u_1} [inst : TopologicalSpace X] [Infinite X] [DiscreteTopology X], ¬Continuous ⇑CofiniteTopology.of.symm

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.

Defined in

Mathlib.Topology.Compactification.OnePoint.Basic

Cited by

1 results in Mathlib

Foundations

Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceInfiniteDiscreteTopology