edist_le_range_sum_edist — Mathlib

English

Triangle inequality in the range version: for a sequence f: Nat → α, edist(f(0), f(n)) is bounded by the sum of edist(f(i), f(i+1)) for i in 0..n-1.

Русский

Неравенство треугольника в диапазонной формулировке: distance между f(0) и f(n) ограничено суммой edist(f(i), f(i+1)) для i от 0 до n-1.

LaTeX

$$$\forall f:\mathbb{N}\to \alpha,\; edist(f(0), f(n)) \le \sum_{i=0}^{n-1} edist(f(i), f(i+1)).$$$

Lean4

/-- The triangle (polygon) inequality for sequences of points; `Finset.range` version. -/
theorem edist_le_range_sum_edist (f : ℕ → α) (n : ℕ) :
    edist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, edist (f i) (f (i + 1)) :=
  Nat.Ico_zero_eq_range ▸ edist_le_Ico_sum_edist f (Nat.zero_le n)

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