lean_workbook_plus_60636

Proved

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

Prove the Nested Interval Theorem: if $I_n=[a_n,b_n]$ are a sequence of closed bounded intervals such that $I_1\supseteq I_2\subseteq I_3\supseteq\cdots,$ then $\bigcup_{n=1}^{\infty}I_n$ is nonempty.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_60636 (a b : ℕ → ℝ) (hab : ∀ n, a n ≤ b n) (h1 : ∀ n, [a n, b n] ⊆ [a (n + 1), b (n + 1)]): ∃ x, ∀ n, x ∈ [a n, b n]   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph