Theorem exists_finite_cover_balls_of_isCompact_closure

Modification history

2025-03-19 19:40
Mathlib/Topology/MetricSpace/Pseudo/Basic.lean
feat: covering a relatively compact set by balls (#23108) …
Added exists_finite_cover_balls_of_isCompact_closureView on Github →