English
If for a sequence s:β→α the distances dist(s_n,s_m) are bounded above by b_n whenever n≤m, and b tends to 0, then s is Cauchy.
Русский
Если для последовательности s:β→α расстояния dist(s_n,s_m) сверху ограничены b_n при n≤m, и b_n → 0, тогда s — последовательность Коши.
LaTeX
$$$\\displaystyle \\left(\\forall n,m,\\, n\\le m\\Rightarrow \\operatorname{dist}(s_n,s_m)\\le b_n\\right) \\wedge \\big(\\lim_{\\to} b = 0\\big) \\Rightarrow \\text{CauchySeq}(s).$$$
Lean4
/-- If the distance between `s n` and `s m`, `n ≤ m` is bounded above by `b n`
and `b` converges to zero, then `s` is a Cauchy sequence. -/
theorem cauchySeq_of_le_tendsto_0' {s : β → α} (b : β → ℝ) (h : ∀ n m : β, n ≤ m → dist (s n) (s m) ≤ b n)
(h₀ : Tendsto b atTop (𝓝 0)) : CauchySeq s :=
Metric.cauchySeq_iff'.2 fun ε ε0 =>
(h₀.eventually (gt_mem_nhds ε0)).exists.imp fun N hN n hn =>
calc
dist (s n) (s N) = dist (s N) (s n) := dist_comm _ _
_ ≤ b N := (h _ _ hn)
_ < ε := hN
