lean_workbook_plus_55601

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that any bounded sequence in $\mathbb{R}$ has a limit point.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_55601 (b : ℕ → ℝ) (h₁ : ∃ a, ∀ n, |b n| < a) : ∃ a, a ∈ {a : ℝ | ∃ n, b n ∈ Set.Icc a (a + 1)}   :=  by sorry

Source