dist_triangle4 — Mathlib

English

For all x,y,z,w ∈ α, dist(x,w) ≤ dist(x,y) + dist(y,z) + dist(z,w).

Русский

Для любых x,y,z,w ∈ α верно: dist(x,w) ≤ dist(x,y) + dist(y,z) + dist(z,w).

LaTeX

$$$dist(x,w) \le dist(x,y) + dist(y,z) + dist(z,w)$$$

Lean4

theorem dist_triangle4 (x y z w : α) : dist x w ≤ dist x y + dist y z + dist z w :=
  calc
    dist x w ≤ dist x z + dist z w := dist_triangle x z w
    _ ≤ dist x y + dist y z + dist z w := by gcongr; apply dist_triangle x y z

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