mathlib

c7841093 - feat(topology/metric_space/hausdorff_distance): Add lemmas about frontiers of thickenings. (#17358)

feat(topology/metric_space/hausdorff_distance): Add lemmas about frontiers of thickenings. (#17358) Remove an unneeded hypothesis from lemma `frontier_thickening_subset` and add a couple of other lemmas about frontiers of thickenings. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>