Theorem Metric.isCompact_closure_ball

Modification history

2026-10-20 13:30
Mathlib/Topology/MetricSpace/Bounded.lean
feat: add some lemmas that closures of some sets are compact (#39382) …
Added Metric.isCompact_closure_ballView on Github →