edist_vsub_vsub_le — Mathlib

English

For p1,p2,p3,p4 ∈ P, edist(p1 −ᵥ p2, p3 −ᵥ p4) ≤ edist(p1,p3) + 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 edist_vsub_vsub_le (p₁ p₂ p₃ p₄ : P) : edist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ edist p₁ p₃ + edist p₂ p₄ :=
  by
  simp only [edist_nndist]
  norm_cast
  apply dist_vsub_vsub_le

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