hausdorffDist_comm — Mathlib

English

The Hausdorff distance is symmetric: hausdorffDist(s, t) = hausdorffDist(t, s).

Русский

Расстояние Хаусдорфа симметрично: hausdorffDist(s, t) = hausdorffDist(t, s).

LaTeX

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

Lean4

/-- The Hausdorff distances from `s` to `t` and from `t` to `s` coincide. -/
theorem hausdorffDist_comm : hausdorffDist s t = hausdorffDist t s := by simp [hausdorffDist, hausdorffEdist_comm]

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