Commit 2025-12-30 20:35 3e3d4c76

View on Github →

feat: UniformSpace.subset_countable_closure_of_almost_dense_set (#32849) Add the new theorem UniformSpace.subset_countable_closure_of_almost_dense_set and golf the PseudoEMetricSpace version with it. Move some stuff around:

IsSeparable.exists_countable_dense_subset and IsSeparable.separableSpace are generalized to pseudometrizable spaces and moved to Metrizable/Basic.
TotallyBounded.isSeparable is moved to UniformSpace/Cauchy
EMetric.subset_countable_closure_of_almost_dense_set is moved to EMetric/Basic

Estimated changes

Modified Mathlib/Topology/EMetricSpace/Basic.lean

added theorem EMetric.subset_countable_closure_of_almost_dense_set

deleted theorem TopologicalSpace.IsSeparable.exists_countable_dense_subset

deleted theorem TopologicalSpace.IsSeparable.separableSpace

Modified Mathlib/Topology/EMetricSpace/Defs.lean

deleted theorem EMetric.subset_countable_closure_of_almost_dense_set

Modified Mathlib/Topology/MetricSpace/Pseudo/Basic.lean

Modified Mathlib/Topology/Metrizable/Basic.lean

added theorem TopologicalSpace.IsSeparable.exists_countable_dense_subset

added theorem TopologicalSpace.IsSeparable.separableSpace

Modified Mathlib/Topology/Metrizable/Uniformity.lean

deleted theorem TotallyBounded.isSeparable

Modified Mathlib/Topology/UniformSpace/Basic.lean

Modified Mathlib/Topology/UniformSpace/Cauchy.lean

added theorem TotallyBounded.isSeparable

added theorem UniformSpace.secondCountable_of_almost_dense_set

added theorem UniformSpace.subset_countable_closure_of_almost_dense_set