hausdorffDist_nonneg

Mathlib.Topology.MetricSpace.HausdorffDistance

URI: https://scilib.ai/kg/mathlib#Metric.hausdorffDist_nonneg

English

The Hausdorff distance is nonnegative: hausdorffDist(s, t) ≥ 0 for all sets s, t.

Русский

Расстояние Хаусдорфа неотрицательно: hausdorffDist(s, t) ≥ 0 для любых множеств s, t.

LaTeX

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

Lean4

/-- The Hausdorff distance is nonnegative. -/
theorem hausdorffDist_nonneg : 0 ≤ hausdorffDist s t := by simp [hausdorffDist]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru