nndist_eq_zero — Mathlib

English

The nonnegative distance vanishes exactly when x = y.

Русский

Ненулевое расстояние равно нулю тогда и только тогда, когда x = y.

LaTeX

$$nndist\;x\;y = 0 \leftrightarrow x = y$$

Lean4

/-- Characterize the equality of points as the vanishing of the nonnegative distance -/
@[simp]
theorem nndist_eq_zero {x y : γ} : nndist x y = 0 ↔ x = y := by
  simp only [NNReal.eq_iff, ← dist_nndist, NNReal.coe_zero, dist_eq_zero]

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