infDist_zero_of_mem — Mathlib

English

The minimal distance to a singleton is the distance to its unique point.

Русский

Минимальное расстояние до множества, состоящего из одной точки, равно расстоянию до этой точки.

LaTeX

$$$ \operatorname{infDist}(x, \{y\}) = \operatorname{dist}(x,y) $$$

Lean4

/-- The minimal distance of a point to a set containing it vanishes. -/
theorem infDist_zero_of_mem (h : x ∈ s) : infDist x s = 0 := by simp [infEdist_zero_of_mem h, infDist]

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