dist_vadd_cancel_right — Mathlib

English

In a NormedAddTorsor, left translation by v preserves the nonnegative distance: nndist(v +ᵥ x, v +ᵥ y) = nndist x y.

Русский

Левое сдвигающее действие на векторе v сохраняет расстояние: nndist(v +ᵥ x, v +ᵥ y) = nndist(x, y).

LaTeX

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

Lean4

@[simp]
theorem dist_vadd_cancel_right (v₁ v₂ : V) (x : P) : dist (v₁ +ᵥ x) (v₂ +ᵥ x) = dist v₁ v₂ := by
  rw [dist_eq_norm_vsub V, dist_eq_norm, vadd_vsub_vadd_cancel_right]

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