mathlib

395e2755 - chore(topology/metric_space/basic): +1 version of Heine-Borel (#11127)

chore(topology/metric_space/basic): +1 version of Heine-Borel (#11127) * Mark `metric.is_compact_of_closed_bounded` as "Heine-Borel" theorem too. * Add `metric.bounded.is_compact_closure`.