English
Let α be a metric space and consider NonemptyCompacts α. The metric on this space is given by the Hausdorff distance between the underlying compact sets. Thus for any x,y ∈ NonemptyCompacts α, dist(x,y) equals the Hausdorff distance between the sets x and y.
Русский
Пусть α — метрическое пространство и рассмотрим пространство непустых компактов α. Метрика на этом пространстве задаётся расстоянием Хаусдорфа между соответствующими компактными подмножествами. Для любых x,y ∈ NonemptyCompacts α выполняется dist(x,y) = hausdorffDist (x) y.
LaTeX
$$$\operatorname{dist}(x,y)=\operatorname{hausdorffDist}(x:y)$$$
Lean4
/-- The distance on `NonemptyCompacts α` is the Hausdorff distance, by construction -/
theorem dist_eq {x y : NonemptyCompacts α} : dist x y = hausdorffDist (x : Set α) y :=
rfl
