hausdorffDist_triangle — Mathlib

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

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