mathlib3

858a10cf - feat(analysis/convex/body): endow with Hausdorff metric (#16338)

feat(analysis/convex/body): endow with Hausdorff metric (#16338) Endows the type of convex bodies with the Hausdorff pseudo-metric. If the underlying vector space is normed instead of only seminormed, this gives rise to the Hausdorff metric. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>