eq_of_nndist_eq_zero — Mathlib

English

If the nonnegative distance between x and y is zero, then x = y.

Русский

Если ненулевой (невырожденный) расстояние между x и y равно нулю, то x = y.

LaTeX

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

Lean4

/-- Deduce the equality of points from the vanishing of the nonnegative distance -/
theorem eq_of_nndist_eq_zero {x y : γ} : nndist x y = 0 → x = y := by
  simp only [NNReal.eq_iff, ← dist_nndist, imp_self, NNReal.coe_zero, dist_eq_zero]

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