mathlib

2e83d617 - feat(topology/metric_space/hausdorff_distance): Thickening the closure (#13515)

feat(topology/metric_space/hausdorff_distance): Thickening the closure (#13515) `thickening δ (closure s) = thickening δ s` and other simple lemmas. Also rename `inf_edist_le_inf_edist_of_subset` to `inf_edist_anti` and make arguments to `mem_thickening_iff` implicit.