hausdorffDist_triangle' — Mathlib

English

Replacing a set by its closure does not change the Hausdorff distance: hausdorffDist(s, closure(s)) = hausdorffDist(s, s).

Русский

Замена множества его замыканием не меняет расстояние Хаусдорфа: hausdorffDist(s, closure(s)) = hausdorffDist(s, s).

LaTeX

$$$\operatorname{hausdorffDist}(\overline{s}, s) = \operatorname{hausdorffDist}(s,s).$$$

Lean4

/-- The Hausdorff distance satisfies the triangle inequality. -/
theorem hausdorffDist_triangle' (fin : hausdorffEdist t u ≠ ⊤) :
    hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u :=
  by
  rw [hausdorffEdist_comm] at fin
  have I : hausdorffDist u s ≤ hausdorffDist u t + hausdorffDist t s := hausdorffDist_triangle fin
  simpa [add_comm, hausdorffDist_comm] using I

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