English
There is a metric space structure on NonemptyCompacts α induced by the Hausdorff distance, provided the sets are nonempty and compact.
Русский
Для NonemptyCompacts α существует метрическое пространство, задаваемое расстоянием Хаусдорфа между множестами, если они непустые и компактные.
LaTeX
$$$\\text{MetricSpace}(\\text{NonemptyCompacts }\\alpha)$, с метрикой $d(A,B)=\\operatorname{hausdorffEdist}(A,B)$, где $A,B$ непусты и компактны.$$
Lean4
/-- `NonemptyCompacts α` inherits a metric space structure, as the Hausdorff
edistance between two such sets is finite. -/
instance metricSpace : MetricSpace (NonemptyCompacts α) :=
EMetricSpace.toMetricSpace fun x y =>
hausdorffEdist_ne_top_of_nonempty_of_bounded x.nonempty y.nonempty x.isCompact.isBounded y.isCompact.isBounded
