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`.





leanprover-community/mathlib,leanprover-community/mathlib