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

• Willard's General Topology

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) : 2 ^ Cardinal.mk ↑s ≤ 2 ^ Cardinal.mk ↑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) : Cardinal.mk ↑s < 2 ^ Cardinal.mk ↑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] : 2 ^ Cardinal.mk ↑s ≤ Cardinal.continuum

theorem IsClosed.mk_lt_continuum {X : Type u} [TopologicalSpace X] [TopologicalSpace.SeparableSpace X] [NormalSpace X] {s : Set X} (hs : IsClosed s) [DiscreteTopology ↑s] : Cardinal.mk ↑s < Cardinal.continuum

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) : ¬NormalSpace X

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.