English
The Hausdorff distance between two sets s and t is the least nonnegative real number r such that s ⊆ N_r(t) and t ⊆ N_r(s); if such r does not exist, define the distance as 0.
Русский
Расстояние Хаусдорфа между двумя множествами s и t есть наименьшее неотрицательное число r такое, что s ⊆ N_r(t) и t ⊆ N_r(s); если такого r не существует, определить расстояние равным 0.
LaTeX
$$$\operatorname{hausdorffDist}(s,t)=\operatorname{toReal}(\operatorname{hausdorffEdist}(s,t)).$$$
Lean4
/-- The Hausdorff distance between two sets is the smallest nonnegative `r` such that each set is
included in the `r`-neighborhood of the other. If there is no such `r`, it is defined to
be `0`, arbitrarily. -/
def hausdorffDist (s t : Set α) : ℝ :=
ENNReal.toReal (hausdorffEdist s t)
