Theorem EMetric.secondCountable_of_sigmaCompact

Modification history

2023-11-07 10:06
Mathlib/Topology/EMetricSpace/Basic.lean
feat: Urysohn lemma in regular locally compact spaces (#8124) …
Deleted EMetric.secondCountable_of_sigmaCompactView on Github →
2023-03-03 08:09
Mathlib/Topology/MetricSpace/EMetricSpace.lean
feat: port Topology.MetricSpace.EMetricSpace (#2407)
Added EMetric.secondCountable_of_sigmaCompactView on Github →