Commit 2026-08-04 14:32 1c3257b2

chore(Topology): state Heine–Borel theorem for metric spaces (#42241) Changes the assumptions of isCompact_iff_isClosed_bounded from [PseudoMetricSpace α] [T2Space α] to [MetricSpace α], giving the usual metric-space formulation of the Heine–Borel theorem. This requires importing Mathlib.Topology.MetricSpace.Basic, which provides MetricSpace.instT0Space. Together with the regularity of uniform spaces, this allows T2Space α to be inferred from MetricSpace α, as needed to show that compact sets are closed.

instance (priority := 100) _root_.MetricSpace.instT0Space : T0Space γ where
  t0 _ _ h := eq_of_dist_eq_zero <| Metric.inseparable_iff.1 h