lipschitz_infNndist_pt — Mathlib

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

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