instMetricSpace — Mathlib

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

Похожие утверждения