dist_triangle4_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem dist_triangle4_left (x₁ y₁ x₂ y₂ : α) : dist x₂ y₂ ≤ dist x₁ y₁ + (dist x₁ x₂ + dist y₁ y₂) :=
  by
  rw [add_left_comm, dist_comm x₁, ← add_assoc]
  apply dist_triangle4

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