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.
References #
theorem
IsClosed.two_pow_mk_le_two_pow_mk_dense
{X : Type u}
[TopologicalSpace X]
[NormalSpace X]
{s d : Set X}
(hs : IsClosed s)
[DiscreteTopology ↑s]
(hd : Dense d)
:
Let s be a closed set in a normal space and d be a dense set. If the induced topology on s
is discrete, then 𝒫 s has cardinality less than or equal to 𝒫 d.
theorem
IsClosed.mk_lt_two_pow_mk_dense
{X : Type u}
[TopologicalSpace X]
[NormalSpace X]
{s d : Set X}
(hs : IsClosed s)
[DiscreteTopology ↑s]
(hd : Dense d)
:
theorem
IsClosed.two_pow_mk_lt_continuum
{X : Type u}
[TopologicalSpace X]
[TopologicalSpace.SeparableSpace X]
[NormalSpace X]
{s : Set X}
(hs : IsClosed s)
[DiscreteTopology ↑s]
:
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.
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.