infDist_eq_iInf — Mathlib

English

The distance to a set equals the infimum of distances to its elements, i.e., infEdist x s = iInf (dist x y) over y ∈ s.

Русский

Расстояние до множества равно би́нному инфиму dist x y по y ∈ s.

LaTeX

$$$ \operatorname{infEdist}(x,s) = \operatorname{iInf}_{y: s} \operatorname{dist}(x,y) $$$

Lean4

theorem infDist_eq_iInf : infDist x s = ⨅ y : s, dist x y :=
  by
  rw [infDist, infEdist, iInf_subtype', ENNReal.toReal_iInf]
  · simp only [dist_edist]
  · finiteness

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