nndist_vadd_vadd_le — Mathlib

English

For v,v' ∈ V and p,p' ∈ P, the nonnegative distance between v +ᵥ p and v' +ᵥ p' is bounded by the sum of the respective nonnegative distances: nndist(v +ᵥ p, v' +ᵥ p') ≤ nndist(v,v') + nndist(p,p').

Русский

Для v,v' ∈ V и p,p' ∈ P выполняется: nndist(v +ᵥ p, v' +ᵥ p') ≤ nndist(v,v') + nndist(p,p').

LaTeX

$$$\operatorname{nndist}(v +ᵥ p, v' +ᵥ p') \le \operatorname{nndist}(v,v') + \operatorname{nndist}(p,p')$$$

Lean4

theorem nndist_vadd_vadd_le (v v' : V) (p p' : P) : nndist (v +ᵥ p) (v' +ᵥ p') ≤ nndist v v' + nndist p p' :=
  dist_vadd_vadd_le _ _ _ _

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