Theorem Metric.isCompact_iff_isClosed_bounded
Modification history
2026-08-04 14:32
Mathlib/Topology/MetricSpace/Bounded.lean
chore(Topology): state Heine–Borel theorem for metric spaces (#42241) …
Modified Metric.isCompact_iff_isClosed_boundedView on Github →