hausdorffEdist_comm — Mathlib

English

Hausdorff edistance is symmetric: hausdorffEdist s t = hausdorffEdist t s.

Русский

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

LaTeX

$$$\operatorname{hausdorffEdist}(s,t) = \operatorname{hausdorffEdist}(t,s)$$$

Lean4

/-- The Hausdorff edistances of `s` to `t` and of `t` to `s` coincide. -/
theorem hausdorffEdist_comm : hausdorffEdist s t = hausdorffEdist t s := by simp only [hausdorffEdist_def];
  apply sup_comm

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