TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Bolzano-Weierstrass: every bounded real sequence has a convergent subsequence

Statement

Every bounded sequence of reals has a convergent subsequence: if $(x_k)$ is a sequence of reals and there is $M \in \mathbb{R}$ with $|x_k| \le M$ for every $k \in \mathbb{N}$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences), then there is a strictly increasing $n : \mathbb{N} \to \mathbb{N}$ and a real $L$ with $x_{n_j} \to L$ .

Equivalently: the subsequential limit set of a bounded sequence is nonempty (Subsequential limit of a real sequence, and the subsequential limit set).

The theorem is the exact repair of the false claim that a bounded sequence converges. A bounded sequence need not converge, and the alternating sequence is the standing witness; what boundedness does force is that some subsequence converges. The converse of the theorem is false, and badly so: a sequence with a convergent subsequence need not be bounded.

Facts & Assumptions

Given: A sequence $(x_k)$ of reals and a real $M$ with $|x_k| \le M$ for every $k \in \mathbb{N}$ .

[L1]

Every sequence of reals has a monotone subsequence (Every real sequence has a monotone subsequence (the peak / rising-sun lemma)).

[L2]

A monotone sequence of reals converges if and only if it is bounded (A monotone sequence converges if and only if it is bounded).

[L3]

A subsequence $(x_{n_j})$ of $(x_k)$ along a strictly increasing $n$ is again a sequence of reals, and each of its terms is a term of $(x_k)$ ; a sequence is bounded when some $M$ satisfies $|{\cdot}| \le M$ at every index (Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L4]

Monotone means nondecreasing or nonincreasing (Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences).

[L5]

$L$ is a subsequential limit of $(x_k)$ when some subsequence of $(x_k)$ converges to $L$ (Subsequential limit of a real sequence, and the subsequential limit set).

Proof

technique · direct

1.1

By [L1] fix a strictly increasing $n : \mathbb{N} \to \mathbb{N}$ such that the subsequence $(x_{n_j})$ is monotone; no hypothesis on $(x_k)$ is needed for this step.

givenL1L4choose

2.1

$(x_{n_j})$ is bounded: each of its terms is a term of $(x_k)$ , so $|x_{n_j}| \le M$ for every $j$ , with the same $M$ .

step 1.1givenL3

3.1

Being monotone and bounded, $(x_{n_j})$ converges; write $L$ for its limit.

step 1.1step 2.1L2

4.1

So $(x_k)$ has a convergent subsequence, and $L$ is a subsequential limit of $(x_k)$ ; in particular the subsequential limit set of a bounded sequence is nonempty.

step 3.1L5∎

Remarks

The proof is two citations, and that is the point of the page order. All the work sits in Every real sequence has a monotone subsequence (the peak / rising-sun lemma), which needs nothing about $\mathbb{R}$ beyond trichotomy, and in A monotone sequence converges if and only if it is bounded, which is where the least-upper-bound property is actually spent. Splitting the argument this way isolates the use of completeness in a single place instead of burying it in a bisection.
Bisection is the other standard proof and is not used here. Halving the interval $[-M, M]$ repeatedly and keeping a half containing infinitely many terms produces a nested sequence of intervals whose lengths tend to $0$ , and A nested sequence of nonempty closed bounded intervals has nonempty intersection, and the intersection is a single point exactly when the lengths tend to $0$ then yields the limit. That route is available in this library, since the nested interval property is proved on this page, but it needs an extra argument to choose the terms and to see that the chosen indices increase, whereas the monotone-subsequence route needs neither.
The limit is not determined by the theorem. A bounded sequence may have many subsequential limits, and the theorem asserts only that there is at least one. Which subsequential limits exist, and that there is a largest and a smallest, is the subject of the $\limsup$ page.
Boundedness is sufficient but not necessary. The converse fails, by FALSE: a sequence with a convergent subsequence is bounded (the converse of Bolzano-Weierstrass) and its witness The sequence $1, 1, 2, 1, 3, 1, 4, \dots$ is unbounded and has a convergent subsequence ↗: a wildly unbounded sequence can still have a constant, hence convergent, subsequence.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 59 results over 13 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Bolzano-Weierstrass theorem (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 3 (Thm 3.6(b)) (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed., §6.6 (Thm 6.6.8) (standard reference, not scraped)
J. Lebl, Basic Analysis I, §2.3 (Thm 2.3.8) (standard reference, not scraped)