isGLB_infDist

Mathlib.Topology.MetricSpace.HausdorffDistance

URI: https://scilib.ai/kg/mathlib#Metric.isGLB_infDist

← MathLib Explorer

English

infEdist x s = ∞ iff s = ∅.

Русский

infEdist x s = ∞ тогда и только тогда, когда s = ∅.

LaTeX

$$$ \operatorname{infEdist}(x,s) = \infty \iff s = \varnothing $$$

Lean4

theorem isGLB_infDist (hs : s.Nonempty) : IsGLB ((dist x ·) '' s) (infDist x s) := by
  simpa [infDist_eq_iInf, sInf_image'] using isGLB_csInf (hs.image _) ⟨0, by simp [lowerBounds]⟩

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

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

Разделы

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

Аффилиация

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