nndist_vsub_cancel_left — Mathlib

English

For x,y,z ∈ P, the nonnegative distance between x −ᵥ y and x −ᵥ z equals the nonnegative distance between y and z: nndist(x −ᵥ y, x −ᵥ z) = nndist(y, z).

Русский

Пусть x,y,z ∈ P. Непрерывное неотрицательное расстояние между x −ᵥ y и x −ᵥ z равно между y и z: nndist(x −ᵥ y, x −ᵥ z) = nndist(y, z).

LaTeX

$$$\operatorname{nndist}(x -ᵥ y, x -ᵥ z) = \operatorname{nndist}(y,z)$$$

Lean4

@[simp]
theorem nndist_vsub_cancel_left (x y z : P) : nndist (x -ᵥ y) (x -ᵥ z) = nndist y z :=
  NNReal.eq <| dist_vsub_cancel_left _ _ _

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