Theorem TopologicalSpace.IsSeparable.separableSpace

Modification history

2025-12-30 20:35
Mathlib/Topology/EMetricSpace/Basic.lean
feat: `UniformSpace.subset_countable_closure_of_almost_dense_set` (#32849) …
Modified TopologicalSpace.IsSeparable.separableSpaceView on Github →
2025-02-11 11:19
Mathlib/Topology/EMetricSpace/Basic.lean
chore(Topology/(E)MetricSpace): move import of `Topology.Bases` downstream (#21657) …
Modified TopologicalSpace.IsSeparable.separableSpaceView on Github →
2024-08-16 01:08
Mathlib/Topology/EMetricSpace/Basic.lean
chore: splitting up metric spaces files (#15790)
Modified TopologicalSpace.IsSeparable.separableSpaceView on Github →
2023-03-03 17:48
Mathlib/Topology/MetricSpace/EMetricSpace.lean
feat: port Topology.MetricSpace.Basic (#2425)
Added TopologicalSpace.IsSeparable.separableSpaceView on Github →