dist_vsub_cancel_left — Mathlib

English

Let x,y,z ∈ P. The distance is invariant under left translation by x: dist(x −ᵥ y, x −ᵥ z) = dist(y, z).

Русский

Пусть x,y,z ∈ P. Расстояние сохраняется при левой транспозиции на x: dist(x −ᵥ y, x −ᵥ z) = dist(y, z).

LaTeX

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

Lean4

@[simp]
theorem dist_vsub_cancel_left (x y z : P) : dist (x -ᵥ y) (x -ᵥ z) = dist y z := by
  rw [dist_eq_norm, vsub_sub_vsub_cancel_left, dist_comm, dist_eq_norm_vsub V]

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