English
Convex bodies in a fixed seminormed space form a pseudo-metric space under the Hausdorff distance.
Русский
Выпуклые тела в фиксированном семиномоду пространства образуют псевдометрическое пространство по метрике Хаусдорфа.
LaTeX
$$$\\text{ConvexBody}(V)$ is equipped with a pseudo-metric $\\operatorname{dist}(K,L)=\\mathrm{hausdorffDist}(K,L)$.$$
Lean4
/-- Convex bodies in a fixed seminormed space $V$ form a pseudo-metric space under the Hausdorff
metric. -/
noncomputable instance : PseudoMetricSpace (ConvexBody V)
where
dist K L := Metric.hausdorffDist (K : Set V) L
dist_self _ := Metric.hausdorffDist_self_zero
dist_comm _ _ := Metric.hausdorffDist_comm
dist_triangle _ _ _ := Metric.hausdorffDist_triangle hausdorffEdist_ne_top
