mathlib

21c9d3b3 - feat(topology/metric_space/hausdorff_distance): add more topological properties API to thickenings (#10661)

feat(topology/metric_space/hausdorff_distance): add more topological properties API to thickenings (#10661) More lemmas about thickenings, especially topological properties, still 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>