infEdist_biUnion

Mathlib.Topology.MetricSpace.HausdorffDistance

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

← MathLib Explorer

English

For any index, the infEdist over a union equals the infimum over infEdist of each member.

Русский

Для индекса верхнее сведение: infEdist по i-Union = infInfEdist по i.

LaTeX

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

Lean4

theorem infEdist_biUnion {ι : Type*} (f : ι → Set α) (I : Set ι) (x : α) :
    infEdist x (⋃ i ∈ I, f i) = ⨅ i ∈ I, infEdist x (f i) := by simp only [infEdist_iUnion]

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

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

Разделы

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

Аффилиация

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