edist_vadd_vadd_le — Mathlib

English

For p1,p2,p3,p4 ∈ P, nndist(p1 −ᵥ p2, p3 −ᵥ p4) ≤ nndist(p1,p3) + nndist(p2,p4).

Русский

Для p1,p2,p3,p4 ∈ P: nndist(p1 −ᵥ p2, p3 −ᵥ p4) ≤ nndist(p1,p3) + nndist(p2,p4).

LaTeX

$$$\operatorname{nndist}(p_1 -ᵥ p_2, p_3 -ᵥ p_4) \le \operatorname{nndist}(p_1,p_3) + \operatorname{nndist}(p_2,p_4)$$$

Lean4

theorem edist_vadd_vadd_le (v v' : V) (p p' : P) : edist (v +ᵥ p) (v' +ᵥ p') ≤ edist v v' + edist p p' :=
  by
  simp only [edist_nndist]
  norm_cast
  apply dist_vadd_vadd_le

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