English
For a Cauchy sequence u and a positive sequence b, there exists a strictly increasing f such that for all n, and all m≥f(n), we have dist(u_m, u_{f(n)}) < b_n.
Русский
Для последовательности Коши u и положительной последовательности b существует строго возрастающая подпоследовательность f, такая что для всех n и всех m≥f(n) выполняется dist(u_m, u_{f(n)}) < b_n.
LaTeX
$$$\\exists f: \\mathbb{N} \\to \\mathbb{N},\\; \\text{StrictMono}(f) \\land \\forall n, \\forall m \\ge f(n), \\operatorname{dist}(u_m,u_{f(n)}) < b(n).$$$
Lean4
theorem exists_subseq_bounded_of_cauchySeq (u : ℕ → α) (hu : CauchySeq u) (b : ℕ → ℝ) (hb : ∀ n, 0 < b n) :
∃ f : ℕ → ℕ, StrictMono f ∧ ∀ n, ∀ m ≥ f n, dist (u m) (u (f n)) < b n :=
by
rw [cauchySeq_iff] at hu
have hu' : ∀ k, ∀ᶠ (n : ℕ) in atTop, ∀ m ≥ n, dist (u m) (u n) < b k :=
by
intro k
rw [eventually_atTop]
obtain ⟨N, hN⟩ := hu (b k) (hb k)
exact ⟨N, fun m hm r hr => hN r (hm.trans hr) m hm⟩
exact Filter.extraction_forall_of_eventually hu'
