dist_vadd_left — Mathlib

English

Left-right symmetry: the distance between x and y after translating by v₁ then v₂ equals the distance between v₁ and v₂.

Русский

Симметрия расстояний: расстояние между v₁ +ᵥ x и v₂ +ᵥ x равно расстоянию между v₁ и v₂.

LaTeX

$$nndist (v₁ +ᵥ x) (v₂ +ᵥ x) = nndist v₁ v₂$$

Lean4

@[simp]
theorem dist_vadd_left (v : V) (x : P) : dist (v +ᵥ x) x = ‖v‖ := by simp [dist_eq_norm_vsub V _ x]

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