dist_le_tsum_dist_of_tendsto₀ — Mathlib

English

For a fixed n, dist(f(n), a) ≤ tsum of distances from n onward: dist(f(n), f(n+1)) + dist(f(n+1), f(n+2)) + ...

Русский

Для фиксированного n верно: dist(f(n), a) ≤ сумма расстояний между соседними членами от n далее.

LaTeX

$$$$\\operatorname{dist}(f(n), a) \\le \\sum_{m=0}^{\\infty} \\operatorname{dist}(f(n+m), f(n+m+1)).$$$$

Lean4

theorem dist_le_tsum_dist_of_tendsto₀ (h : Summable fun n ↦ dist (f n) (f n.succ)) (ha : Tendsto f atTop (𝓝 a)) :
    dist (f 0) a ≤ ∑' n, dist (f n) (f n.succ) := by simpa only [zero_add] using dist_le_tsum_dist_of_tendsto h ha 0

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