infEdist_zero_of_mem

Mathlib.Topology.MetricSpace.HausdorffDistance

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

← MathLib Explorer

English

If x belongs to the set s, then the infimum edistance from x to s is zero.

Русский

Если x принадлежит множеству s, то infEdist x s = 0.

LaTeX

$$$\forall x\, \forall s\,(x \in s \Rightarrow \infEdist x s = 0)$$$

Lean4

/-- If a point `x` belongs to `s`, then its edist to `s` vanishes -/
theorem infEdist_zero_of_mem (h : x ∈ s) : infEdist x s = 0 :=
  nonpos_iff_eq_zero.1 <| @edist_self _ _ x ▸ infEdist_le_edist_of_mem h

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

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

Разделы

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

Аффилиация

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