infDist_empty — Mathlib

English

The minimal distance to the empty set is 0 (same as above).

Русский

Минимальное расстояние до пустого множества равно 0 (то же, что и выше).

LaTeX

$$$ \operatorname{infDist}(x, \varnothing) = 0 $$$

Lean4

/-- The minimal distance to the empty set is 0 (if you want to have the more reasonable
value `∞` instead, use `EMetric.infEdist`, which takes values in `ℝ≥0∞`) -/
@[simp]
theorem infDist_empty : infDist x ∅ = 0 := by simp [infDist]

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