mathlib3

0bc51f02 - feat(topology/metric_space/hausdorff_distance): Thickening a compact inside an open (#14926)

feat(topology/metric_space/hausdorff_distance): Thickening a compact inside an open (#14926) If a compact set is contained in an open set, then we can find a (closed) thickening of it still contained in the open.