nndist_vadd_right — Mathlib

English

Let V act on P by a normed additive torsor structure. For any v ∈ V and x ∈ P, the distance between x and its translate by v equals the norm of v: dist(x, v ⊕ x) = ||v||.

Русский

Пусть V действует на P как нормированная аддитивная торсора. Для любого v ∈ V и x ∈ P расстояние между x и его приращением v ⊕ x равно норме вектора v: dist(x, v ⊕ x) = ||v||.

LaTeX

$$$\operatorname{dist}(x, v \,+\!\!\v x) = \|v\|$$$

Lean4

@[simp]
theorem nndist_vadd_right (v : V) (x : P) : nndist x (v +ᵥ x) = ‖v‖₊ :=
  NNReal.eq <| dist_vadd_right _ _

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