# 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.