le_infEdist

Mathlib.Topology.MetricSpace.HausdorffDistance

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

English

The minimal distance to a union equals the infimum of the minimal distances to each part.

Русский

Минимальное расстояние до объединения равняется инфиминума от расстояний до каждой частu.

LaTeX

$$infEdist x (\\bigcup_i f i) = \\bigwedge_i infEdist x (f i)$$

Lean4

theorem le_infEdist {d} : d ≤ infEdist x s ↔ ∀ y ∈ s, d ≤ edist x y := by simp only [infEdist, le_iInf_iff]

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

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

Разделы

Аффилиация

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