English
The Hausdorff distance satisfies the triangle inequality: hausdorffDist(s, u) ≤ hausdorffDist(s, t) + hausdorffDist(t, u).
Русский
Расстояние Хаусдорфа удовлетворяет неравенству треугольника: hausdorffDist(s,u) ≤ hausdorffDist(s,t) + hausdorffDist(t,u).
LaTeX
$$$\operatorname{hausdorffDist}(s,u) \le \operatorname{hausdorffDist}(s,t) + \operatorname{hausdorffDist}(t,u).$$$
Lean4
/-- The Hausdorff distance satisfies the triangle inequality. -/
theorem hausdorffDist_triangle (fin : hausdorffEdist s t ≠ ⊤) :
hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u :=
by
refine toReal_le_add' hausdorffEdist_triangle (flip absurd fin) (not_imp_not.1 fun h ↦ ?_)
rw [hausdorffEdist_comm] at fin
exact ne_top_of_le_ne_top (add_ne_top.2 ⟨fin, h⟩) hausdorffEdist_triangle