dist_vsub_vsub_le — Mathlib

English

For p1,p2,p3,p4 ∈ P, the distance between p1 −ᵥ p2 and p3 −ᵥ p4 is at most dist(p1,p3) + dist(p2,p4).

Русский

Пусть p1,p2,p3,p4 ∈ P. Тогда dist(p1 −ᵥ p2, p3 −ᵥ p4) ≤ dist(p1,p3) + dist(p2,p4).

LaTeX

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

Lean4

theorem dist_vsub_vsub_le (p₁ p₂ p₃ p₄ : P) : dist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ dist p₁ p₃ + dist p₂ p₄ :=
  by
  rw [dist_eq_norm, vsub_sub_vsub_comm, dist_eq_norm_vsub V, dist_eq_norm_vsub V]
  exact norm_sub_le _ _

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