infDist_singleton — Mathlib

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]

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