mathlib

235e5839 - feat(topology/metric_space/hausdorff_distance): add definition and lemmas about closed thickenings of subsets (#10542)

feat(topology/metric_space/hausdorff_distance): add definition and lemmas about closed thickenings of subsets (#10542) Add definition and basic API about closed 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>