nndist_vsub_vsub_le — Mathlib

English

For p1,p2,p3,p4 ∈ P, the extended distance between p1 −ᵥ p2 and p3 −ᵥ p4 is at most the sum of edist(p1,p3) and edist(p2,p4).

Русский

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

LaTeX

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

Lean4

theorem nndist_vsub_vsub_le (p₁ p₂ p₃ p₄ : P) : nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ nndist p₁ p₃ + nndist p₂ p₄ := by
  simp only [← NNReal.coe_le_coe, NNReal.coe_add, ← dist_nndist, dist_vsub_vsub_le]

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