lean_workbook_plus_24186

Proved

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

The sequence $1$ , $\tfrac12$ , $\tfrac14$ , $\tfrac18$ , ... is bounded (lying in the closed interval $[0,1]$ ).

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_24186 : BddAbove (Set.range (fun n : ℕ => (1/2)^n))   :=  by sorry

Source