dist_eq_norm_vsub — Mathlib

English

The distance in a NormedAddTorsor equals the norm of the vsub between two points.

Русский

Расстояние в нормированном адд-торсоре равно норме вектора разности между двумя точками.

LaTeX

$$dist x y = ‖x −ᵥ y‖$$

Lean4

/-- The distance equals the norm of subtracting two points. In this
lemma, it is necessary to have `V` as an explicit argument; otherwise
`rw dist_eq_norm_vsub` sometimes doesn't work. -/
theorem dist_eq_norm_vsub (x y : P) : dist x y = ‖x -ᵥ y‖ :=
  NormedAddTorsor.dist_eq_norm' x y

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