dist_le_infDist_add_diam

Mathlib.Topology.MetricSpace.HausdorffDistance

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

← MathLib Explorer

English

If s is bounded and y ∈ s, then dist(x,y) ≤ infDist(x,s) + diam(s).

Русский

Если s ограничено и y ∈ s, то dist(x,y) ≤ infDist(x,s) + diam(s).

LaTeX

$$dist(x,y) ≤ infDist x s + diam s$$

Lean4

theorem dist_le_infDist_add_diam (hs : IsBounded s) (hy : y ∈ s) : dist x y ≤ infDist x s + diam s :=
  by
  rw [infDist, diam, dist_edist]
  exact toReal_le_add (edist_le_infEdist_add_ediam hy) (infEdist_ne_top ⟨y, hy⟩) hs.ediam_ne_top

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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