infEdist_le_edist_add_infEdist

Mathlib.Topology.MetricSpace.HausdorffDistance

URI: https://scilib.ai/kg/mathlib#EMetric.infEdist_le_edist_add_infEdist

English

Same bound: infEdist x s ≤ edist x y + infEdist y s.

Русский

Тоже неравенство: infEdist x s ≤ edist x y + infEdist y s.

LaTeX

$$$\infEdist x s \le edist x y + \infEdist y s$$$

Lean4

theorem infEdist_le_edist_add_infEdist : infEdist x s ≤ edist x y + infEdist y s :=
  by
  rw [add_comm]
  exact infEdist_le_infEdist_add_edist

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

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

Разделы

Аффилиация

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