Prove2Me

Bolzano_Weierstrass_Theorem

Proved

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

compactnesslimits-of-sequencesproofwiki

Every bounded sequence of real numbers has a convergent subsequence.

Preamble
import Mathlib.Analysis.Complex.Basic
import Mathlib.Topology.Sequences
Formal statement
import Mathlib.Analysis.Complex.Basic
import Mathlib.Topology.Sequences

theorem Bolzano_Weierstrass_Theorem (x : ℕ → ℝ) (hb : BddAbove (Set.range x) ∧ BddBelow (Set.range x)) : ∃ (phi : ℕ → ℕ) (l : ℝ), StrictMono phi ∧ Filter.Tendsto (x ∘ phi) Filter.atTop (nhds l) := by sorry
Source
https://proofwiki.org/wiki/Bolzano-Weierstrass_Theorem

View graph