Theorems · Theorem · general topology

TopologicalSpace.IsSeparable.exists_countable_dense_subset

∀ {X : Type u_2} [inst : TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] {s : Set X},
  TopologicalSpace.IsSeparable s → ∃ t ⊆ s, t.Countable ∧ s ⊆ closure t

If a set s is separable in a pseudo metrizable space, then it admits a countable dense subset. This is not obvious, as the countable set whose closure covers s given by the definition of separability does not need in general to be contained in s.

Defined in

Mathlib.Topology.Metrizable.Basic

Cited by

2 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpace.PseudoMetrizableSpace