nndist_vadd_cancel_left — Mathlib

English

For any v ∈ V and x, y ∈ P, the nndist between v +ᵥ x and v +ᵥ y equals the nndist between x and y.

Русский

Для любого v ∈ V и x, y ∈ P, расстояние nndist между v +ᵥ x и v +ᵥ y равно расстоянию nndist между x и y.

LaTeX

$$nndist (v +ᵥ x) (v +ᵥ y) = nndist x y$$

Lean4

theorem nndist_vadd_cancel_left (v : V) (x y : P) : nndist (v +ᵥ x) (v +ᵥ y) = nndist x y :=
  NNReal.eq <| dist_vadd_cancel_left _ _ _

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