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