dist_le_range_sum_dist — Mathlib

English

For a function f: N → α, the distance dist(f(0), f(n)) is bounded by the sum of the successive distances dist(f(i), f(i+1)) for i in 0,...,n-1.

Русский

Для функции f: ℕ → α расстояние dist(f(0), f(n)) ограничено суммой последовательных расстояний dist(f(i), f(i+1)) для i=0,...,n-1.

LaTeX

$$$\\text{dist}(f(0), f(n)) \\le \\sum_{i=0}^{n-1} \\text{dist}(f(i), f(i+1))$$$

Lean4

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

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