infEdist_union

Mathlib.Topology.MetricSpace.HausdorffDistance

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

← MathLib Explorer

English

The distance to a union equals the minimum of distances to each component.

Русский

Расстояние до объединения равно минимуму расстояний до компонентов.

LaTeX

$$infEdist x (s ∪ t) = infEdist x s ⊓ infEdist x t$$

Lean4

/-- The edist to a union is the minimum of the edists -/
@[simp]
theorem infEdist_union : infEdist x (s ∪ t) = infEdist x s ⊓ infEdist x t :=
  iInf_union

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

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

Разделы

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

Аффилиация

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