infNndist — Mathlib

English

For any x and subset s of a metric space, the nonnegative distance infNndist(x, s), viewed as a real number, equals the usual distance infDist(x, s).

Русский

Для любых x и множества s в метрическом пространстве неотрицательное расстояние infNndist(x, s), переводя в действительное число, совпадает с обычным infDist(x, s).

LaTeX

$$$(\operatorname{infNndist}(x,s) : \mathbb{R}) = \operatorname{infDist}(x,s).$$$

Lean4

/-- The minimal distance of a point to a set as a `ℝ≥0` -/
def infNndist (x : α) (s : Set α) : ℝ≥0 :=
  ENNReal.toNNReal (infEdist x s)

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