dist_vadd_vadd_le — Mathlib

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')

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