English
Let (X, d) be a metric space and let x, y be points of X. The minimal distance from x to the singleton {y} equals the distance from x to y; that is, infDist x {y} = dist(x, y).
Русский
Пусть (X, d) — метрическое пространство и x, y ∈ X. Минимальное расстояние от x до множества {y} равно расстоянию между x и y: infDist x {y} = dist(x, y).
LaTeX
$$$\\\\infDist x \\\\{ y \\\\} = \\\\operatorname{dist} x y$$$
Lean4
/-- The minimal distance to a singleton is the distance to the unique point in this singleton. -/
@[simp]
theorem infDist_singleton : infDist x { y } = dist x y := by simp [infDist, dist_edist]