dist_triangle4_right — Mathlib

English

For all x1,y1,x2,y2 ∈ α, dist(x1,y1) ≤ dist(x1,x2) + dist(y1,y2) + dist(x2,y2).

Русский

Для любых x1,y1,x2,y2 ∈ α верно: dist(x1,y1) ≤ dist(x1,x2) + dist(y1,y2) + dist(x2,y2).

LaTeX

$$$dist(x_1,y_1) \le dist(x_1,x_2) + dist(y_1,y_2) + dist(x_2,y_2)$$$

Lean4

theorem dist_triangle4_right (x₁ y₁ x₂ y₂ : α) : dist x₁ y₁ ≤ dist x₁ x₂ + dist y₁ y₂ + dist x₂ y₂ :=
  by
  rw [add_right_comm, dist_comm y₁]
  apply dist_triangle4

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