English
For v,v' ∈ V and p,p' ∈ P, the distance between v +ᵥ p and v' +ᵥ p' is at most the sum of distances: dist(v +ᵥ p, v' +ᵥ p') ≤ dist(v,v') + dist(p,p').
Русский
Для v,v' ∈ V и p,p' ∈ P выполняется: dist(v +ᵥ p, v' +ᵥ p') ≤ dist(v,v') + dist(p,p').
LaTeX
$$$\operatorname{dist}(v +ᵥ p, v' +ᵥ p') \le \operatorname{dist}(v,v') + \operatorname{dist}(p,p')$$$
Lean4
theorem dist_vadd_vadd_le (v v' : V) (p p' : P) : dist (v +ᵥ p) (v' +ᵥ p') ≤ dist v v' + dist p p' := by
simpa using dist_triangle (v +ᵥ p) (v' +ᵥ p) (v' +ᵥ p')