dist_eq_norm_vsub' — Mathlib

English

Moreover, nndist between x and y equals the nn-norm of the vsub y −ᵥ x.

Русский

Кроме того, nndist между x и y равен nn‑норме вектора vsub y −ᵥ x.

LaTeX

$$nndist x y = ‖y −ᵥ x‖₊$$

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 = ‖y -ᵥ x‖ :=
  (dist_comm _ _).trans (dist_eq_norm_vsub _ _ _)

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