mathlib

7fec4014 - feat(topology/metric_space/hausdorff_distance): add definition and lemmas about open thickenings of subsets (#10188)

feat(topology/metric_space/hausdorff_distance): add definition and lemmas about open thickenings of subsets (#10188) Add definition and basic API about open thickenings of subsets in metric spaces, in preparation for the portmanteau theorem on characterizations of weak convergence of Borel probability measures. Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>