IsClosed.mk_lt_continuum
theorem IsClosed.mk_lt_continuum :
∀ {X : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace.SeparableSpace X] [inst_2 : NormalSpace X]
{s : Set X}, IsClosed s → ∀ [inst : DiscreteTopology ↑s], Cardinal.mk ↑s < Cardinal.continuum
This theorem states that in any separable and normal topological space 'X', for any closed set 's', if the topological structure induced on 's' is discrete, then the cardinality of 's' is strictly less than the cardinality of the continuum. This is a result relevant to topological spaces and set theory, and the proof follows from a concept related to the Moore plane in topology.
More concisely: In a separable and normal topological space, any closed set with a discrete topology has strictly less cardinality than the continuum.
|
IsClosed.not_normal_of_continuum_le_mk
theorem IsClosed.not_normal_of_continuum_le_mk :
∀ {X : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace.SeparableSpace X] {s : Set X},
IsClosed s → ∀ [inst_2 : DiscreteTopology ↑s], Cardinal.continuum ≤ Cardinal.mk ↑s → ¬NormalSpace X
The theorem `IsClosed.not_normal_of_continuum_le_mk` states that if we have a closed set `s` in a separable topological space `X`, where `s` is endowed with a discrete topology, and the cardinality of `s` is at least as large as the cardinality of the continuum (which is the cardinality of the set of real numbers), then the original space `X` cannot be a normal space. A normal space, in topology, is a topological space in which any two disjoint closed sets can be separated by open sets.
More concisely: If a closed set in a separable topological space with a discrete topology has cardinality equal to or greater than the continuum, then the space cannot be normal.
|