English
The convex bodies in a fixed normed space form a pseudo-metric space with the Hausdorff metric.
Русский
Выпуклые тела в фиксированном нормированном пространстве образуют псевдометрическое пространство по метрике Хаусдорфа.
LaTeX
$$$\\text{ConvexBody}(V)\\text{ is a pseudo-metric space with }d(K,L)=\\mathrm{hausdorffDist}(K,L).$$$
Lean4
/-- Convex bodies in a fixed normed space `V` form a metric space under the Hausdorff metric. -/
noncomputable instance : MetricSpace (ConvexBody V) where
eq_of_dist_eq_zero {K L}
hd := ConvexBody.ext <| (K.isClosed.hausdorffDist_zero_iff_eq L.isClosed hausdorffEdist_ne_top).1 hd