edist_eq — Mathlib

English

The edistance on Closeds agrees with Hausdorff distance: edist s t = hausdorffEdist (s:Set α) t.

Русский

Расстояние edist между замкнутыми множествами совпадает с расстоянием Гаусдорфа: edist s t = hausdorffEdist (s:Set α) t.

LaTeX

$$$\\displaystyle \\operatorname{edist}(s,t) = \\operatorname{hausdorffEdist}(\\{s\\},t).$$$

Lean4

/-- By definition, the edistance on `Closeds α` is given by the Hausdorff edistance -/
theorem edist_eq {s t : Closeds α} : edist s t = hausdorffEdist (s : Set α) t :=
  rfl

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