English
For a sequence f: N → α in a pseudometric space, for any m ≤ n, dist(f(m), f(n)) is bounded by the sum of consecutive distances along the index interval [m, n).
Русский
Для последовательности f: ℕ → α в псевдометрическом пространстве для любого m ≤ n расстояние dist(f(m), f(n)) ограничено суммой последовательных расстояний вдоль отрезка [m, n).
LaTeX
$$$\\text{dist}(f(m), f(n)) \\le \\sum_{i=m}^{n-1} \\text{dist}(f(i), f(i+1))$ для $m \\le n$$$
Lean4
/-- The triangle (polygon) inequality for sequences of points; `Finset.Ico` version. -/
theorem dist_le_Ico_sum_dist (f : ℕ → α) {m n} (h : m ≤ n) :
dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1)) := by
induction n, h using Nat.le_induction with
| base => rw [Finset.Ico_self, Finset.sum_empty, dist_self]
| succ n hle ihn =>
calc
dist (f m) (f (n + 1)) ≤ dist (f m) (f n) + dist (f n) (f (n + 1)) := dist_triangle _ _ _
_ ≤ (∑ i ∈ Finset.Ico m n, _) + _ := (add_le_add ihn le_rfl)
_ = ∑ i ∈ Finset.Ico m (n + 1), _ := by
rw [← Finset.insert_Ico_right_eq_Ico_add_one hle, Finset.sum_insert, add_comm]; simp
