English
A Cauchy sequence indexed by ℕ is bounded in distance: there exists R>0 such that dist(u_m,u_n) < R for all m,n.
Русский
Последовательность Коши, индексированная по ℕ, ограничена по метрике: существует R>0, такое что dist(u_m,u_n) < R для всех m,n.
LaTeX
$$$\\displaystyle \\forall u: \\mathbb{N}\\to X,\\; \\text{CauchySeq}(u)\\Rightarrow \\exists R>0:\\mathbb{R},\\; \\forall m,n:\\mathbb{N},\\; \\operatorname{dist}(u_m,u_n) < R.$$$
Lean4
/-- A Cauchy sequence on the natural numbers is bounded. -/
theorem cauchySeq_bdd {u : ℕ → α} (hu : CauchySeq u) : ∃ R > 0, ∀ m n, dist (u m) (u n) < R :=
by
rcases Metric.cauchySeq_iff'.1 hu 1 zero_lt_one with ⟨N, hN⟩
rsuffices ⟨R, R0, H⟩ : ∃ R > 0, ∀ n, dist (u n) (u N) < R
· exact ⟨_, add_pos R0 R0, fun m n => lt_of_le_of_lt (dist_triangle_right _ _ _) (add_lt_add (H m) (H n))⟩
let R := Finset.sup (Finset.range N) fun n => nndist (u n) (u N)
refine ⟨↑R + 1, add_pos_of_nonneg_of_pos R.2 zero_lt_one, fun n => ?_⟩
rcases le_or_gt N n with h | h
· exact lt_of_lt_of_le (hN _ h) (le_add_of_nonneg_left R.2)
· have : _ ≤ R := Finset.le_sup (Finset.mem_range.2 h)
exact lt_of_le_of_lt this (lt_add_of_pos_right _ zero_lt_one)
