infEdist_singleton

Mathlib.Topology.MetricSpace.HausdorffDistance

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

← MathLib Explorer

English

The infEdist over a biUnion equals the infimum over the indexed family of infEdist.

Русский

infEdist по двойному объединению = infInfEdist по индексам.

LaTeX

$$infEdist x (⋃ i ∈ I, f i) = ⨅ i ∈ I, infEdist x (f i)$$

Lean4

/-- The edist to a singleton is the edistance to the single point of this singleton -/
@[simp]
theorem infEdist_singleton : infEdist x { y } = edist x y :=
  iInf_singleton

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

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

Разделы

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

Аффилиация

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