English
The minimal distance to a set (as a nonnegative real) is 1-Lipschitz with respect to the point: |infNndist(x, s) − infNndist(y, s)| ≤ d(x, y).
Русский
Минимальное расстояние до множества (как неотрицательное число) по перемещению точки является 1-Липшицевой: |infNndist(x, s) − infNndist(y, s)| ≤ d(x, y).
LaTeX
$$$\forall x,y: |\operatorname{infNndist}(x,s)-\operatorname{infNndist}(y,s)| \le d(x,y).$$$
Lean4
/-- The minimal distance to a set (as `ℝ≥0`) is Lipschitz in point with constant 1 -/
theorem lipschitz_infNndist_pt (s : Set α) : LipschitzWith 1 fun x => infNndist x s :=
LipschitzWith.of_le_add fun _ _ => infDist_le_infDist_add_dist