Theorem Metric.exists_finite_isCover_of_totallyBounded

Modification history

2025-11-14 11:52
Mathlib/Topology/MetricSpace/Cover.lean
feat: totally bounded sets have finite covers (#31537) …
Added Metric.exists_finite_isCover_of_totallyBoundedView on Github →