English
The Hausdorff distance satisfies the triangle inequality: d_H(s,u) ≤ d_H(s,t) + d_H(t,u).
Русский
Расстояние Хаусдорфа удовлетворяет неравенству треугольника: d_H(s,u) ≤ d_H(s,t) + d_H(t,u).
LaTeX
$$$ \operatorname{hausdorffEdist}(s,u) \le \operatorname{hausdorffEdist}(s,t) + \operatorname{hausdorffEdist}(t,u) $$$
Lean4
/-- The Hausdorff distance satisfies the triangle inequality. -/
theorem hausdorffEdist_triangle : hausdorffEdist s u ≤ hausdorffEdist s t + hausdorffEdist t u :=
by
rw [hausdorffEdist_def]
simp only [sup_le_iff, iSup_le_iff]
constructor
· change ∀ x ∈ s, infEdist x u ≤ hausdorffEdist s t + hausdorffEdist t u
exact fun x xs =>
calc
infEdist x u ≤ infEdist x t + hausdorffEdist t u := infEdist_le_infEdist_add_hausdorffEdist
_ ≤ hausdorffEdist s t + hausdorffEdist t u := add_le_add_right (infEdist_le_hausdorffEdist_of_mem xs) _
· change ∀ x ∈ u, infEdist x s ≤ hausdorffEdist s t + hausdorffEdist t u
exact fun x xu =>
calc
infEdist x s ≤ infEdist x t + hausdorffEdist t s := infEdist_le_infEdist_add_hausdorffEdist
_ ≤ hausdorffEdist u t + hausdorffEdist t s := (add_le_add_right (infEdist_le_hausdorffEdist_of_mem xu) _)
_ = hausdorffEdist s t + hausdorffEdist t u := by simp [hausdorffEdist_comm, add_comm]
