Not normal topological spaces #
In this file we prove (see IsClosed.not_normal_of_continuum_le_mk) that a separable space with a
discrete subspace of cardinality continuum is not a normal topological space.
theorem
IsClosed.mk_lt_continuum
{X : Type u}
[TopologicalSpace X]
[TopologicalSpace.SeparableSpace X]
[NormalSpace X]
{s : Set X}
(hs : IsClosed s)
[DiscreteTopology ↑s]
:
Let s be a closed set in a separable normal space. If the induced topology on s is discrete,
then s has cardinality less than continuum.
The proof follows https://en.wikipedia.org/wiki/Moore_plane#Proof_that_the_Moore_plane_is_not_normal
theorem
IsClosed.not_normal_of_continuum_le_mk
{X : Type u}
[TopologicalSpace X]
[TopologicalSpace.SeparableSpace X]
{s : Set X}
(hs : IsClosed s)
[DiscreteTopology ↑s]
(hmk : Cardinal.continuum ≤ Cardinal.mk ↑s)
:
Let s be a closed set in a separable space. If the induced topology on s is discrete and s
has cardinality at least continuum, then the ambient space is not a normal space.