English
If for a sequence s:β→α the distances dist(s_n,s_m) for n,m≥N are bounded by b_N with b_N→0, then s is Cauchy.
Русский
Если для последовательности s:β→α расстояния dist(s_n,s_m) при n,m≥N ограничены b_N, и b_N→0, тогда s — Коши.
LaTeX
$$$\\displaystyle \\big(\\forall n,m,N,\\ N\\le n\\to N\\le m\\to \\operatorname{dist}(s_n,s_m)\\le b_N\\big) \\\\Rightarrow \\\\ \\text{Tendsto } b_{\\; } atTop (\\mathcal{N}_0) \\Rightarrow \\text{CauchySeq}(s).$$$
Lean4
/-- If the distance between `s n` and `s m`, `n, m ≥ N` 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 : β, N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N)
(h₀ : Tendsto b atTop (𝓝 0)) : CauchySeq s :=
cauchySeq_of_le_tendsto_0' b (fun _n _m hnm => h _ _ _ le_rfl hnm) h₀
