Theorem TotallyBounded.isSeparable

Modification history

2025-12-30 20:35

Mathlib/Topology/Metrizable/Uniformity.lean

feat: `UniformSpace.subset_countable_closure_of_almost_dense_set` (#32849) …

Modified TotallyBounded.isSeparable View on Github →

2024-04-29 09:02

Mathlib/Topology/Metrizable/Uniformity.lean

feat(UniformSpace) : TotallyBounded + countably generated -> Separable (#12404) …

Added TotallyBounded.isSeparable View on Github →