nndist_vsub_cancel_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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