dist_vsub_cancel_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem dist_vsub_cancel_right (x y z : P) : dist (x -ᵥ z) (y -ᵥ z) = dist x y :=
  (IsometryEquiv.vaddConst z).symm.dist_eq x y

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