triangle_inequality — Mathlib

English

For all n,m,k ∈ ℕ, dist(n,k) ≤ dist(n,m) + dist(m,k).

Русский

Для любых n,m,k ∈ ℕ верно: dist(n,k) ≤ dist(n,m) + dist(m,k).

LaTeX

$$$$ dist(n,k) \le dist(n,m) + dist(m,k). $$$$

Lean4

theorem triangle_inequality (n m k : ℕ) : dist n k ≤ dist n m + dist m k :=
  by
  have : dist n m + dist m k = n - m + (m - k) + (k - m + (m - n)) := by simp [dist, add_comm, add_left_comm, add_assoc]
  rw [this, dist]
  exact add_le_add tsub_le_tsub_add_tsub tsub_le_tsub_add_tsub

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