LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

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

Statement

Every sequence of reals has a monotone subsequence: for every sequence $(x_{k})$ of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences) there is a strictly increasing $n : N \to N$ such that the subsequence $(x_{n_{j}})$ is monotone (Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences).

No hypothesis whatever is placed on $(x_{k})$ : it need not be bounded, and it need not converge. Combined with the corollary later on this page, which converts monotone plus bounded into convergent, this is the whole content of the Bolzano-Weierstrass theorem.

Call an index $n \in N$ a peak of $(x_{k})$ when

$x_{m} \leq x_{n} for every m \geq n,$

that is, when no later term ever exceeds $x_{n}$ . The proof splits on whether peaks occur arbitrarily late or stop occurring, and produces a nonincreasing subsequence in the first case and an increasing one in the second. The picture behind the name is the rising sun shining from the right: the peaks are the points that are not put in shadow by anything to their right.

Facts & Assumptions

Given: A sequence $(x_{k})$ of reals. An index $n \in N$ is called a peak when $x_{m} \leq x_{n}$ for every $m \geq n$ , and $P \subseteq N$ denotes the set of peaks.

[L1]

Recursion theorem: for a set $A$ , an element $a \in A$ and a function $f : A \to A$ there is a unique $g : N \to A$ with $g_{0} = a$ and $g_{σ (j)} = f (g_{j})$ (The recursion theorem).

[L2]

Well-ordering principle: every nonempty subset of $N$ has a least element (The well-ordering principle).

[L3]

Consecutive comparisons suffice for an index map: if $n_{j} < n_{σ (j)}$ for every $j$ then $n$ is strictly increasing (A strictly increasing index map satisfies $n_{k} \geq k$ ).

[L4]

Consecutive comparisons suffice for monotonicity: if $y_{σ (j)} \leq y_{j}$ for every $j$ then $(y_{j})$ is nonincreasing, and if $y_{j} < y_{σ (j)}$ for every $j$ then $(y_{j})$ is increasing; in both cases $(y_{j})$ is monotone (Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences).

[L5]

Subsequences: for strictly increasing $n$ , the composite $(x_{n_{j}})$ is a subsequence of $(x_{k})$ and is again a sequence of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L6]

Order on $N$ : $m < n$ means $m \leq n$ and $m \neq n$ ; the order is total and transitive (Order on the natural numbers, $\leq$ is a linear order on $N$ ).

[L7]

Discreteness: $N < σ (N)$ for every $N \in N$ (Discreteness: $σ (n)$ is the immediate successor).

[L8]

Trichotomy in $R$ : for reals $s, t$ exactly one of $s < t$ , $s = t$ , $s > t$ holds, so the failure of $x_{m} \leq x_{n}$ is $x_{m} > x_{n}$ , and $x_{n} > x_{n}$ is impossible (Order on the reals, Complete ordered field (least-upper-bound property), Ordered field).

Proof

technique · cases

1.1

Case (i). Assume that for every $N \in N$ there is a peak $n$ with $n > N$ .

givenassume-case cofinal

1.2

Case (ii). Assume instead that there is $N_{0} \in N$ such that no $n > N_{0}$ is a peak.

givenassume-case bounded

2.1

In case (i) the set $P$ is nonempty, since the case hypothesis applied to $N = 0$ produces a peak, so $P$ has a least element $p_{0}$ .

step 1.1L2choose

2.2

In case (i), for each $p \in P$ the set ${q \in P : q > p}$ is nonempty, by the case hypothesis applied to $N = p$ ; let $f (p)$ be its least element. This defines $f : P \to P$ with $f (p) > p$ for every $p \in P$ .

step 1.1L2construct

2.3

In case (ii) put $A : = {n \in N : n > N_{0}}$ ; it is nonempty because $σ (N_{0}) > N_{0}$ .

step 1.2L7

3.1

In case (i), the recursion theorem applied to the set $P$ , the element $p_{0}$ and the function $f$ gives $g : N \to P$ with $g_{0} = p_{0}$ and $g_{σ (j)} = f (g_{j})$ ; every $g_{j}$ is a peak and $g_{j} < g_{σ (j)}$ for every $j$ .

step 2.1step 2.2L1

3.2

In case (ii), each $n \in A$ satisfies $n > N_{0}$ and so is not a peak, meaning some $m \geq n$ has $x_{m} > x_{n}$ ; such an $m$ is distinct from $n$ , since $x_{n} > x_{n}$ is impossible, hence $m > n > N_{0}$ and $m \in A$ . The set of such $m$ is therefore a nonempty subset of $A$ ; let $h (n)$ be its least element. This defines $h : A \to A$ with $h (n) > n$ and $x_{h (n)} > x_{n}$ .

step 2.3L2L6L8construct

4.1

In case (i), $g$ is strictly increasing by [L3], so $(x_{g_{j}})$ is a subsequence of $(x_{k})$ .

step 3.1L3L5

4.2

In case (i), for every $j$ the index $g_{σ (j)}$ satisfies $g_{σ (j)} \geq g_{j}$ and $g_{j}$ is a peak, so $x_{g_{σ (j)}} \leq x_{g_{j}}$ ; hence $(x_{g_{j}})$ is nonincreasing, so monotone.

step 3.1L4

4.3

In case (ii), the recursion theorem applied to the set $A$ , the element $σ (N_{0})$ and the function $h$ gives $g^{'} : N \to A$ with $g_{0}^{'} = σ (N_{0})$ and $g_{σ (j)}^{'} = h (g_{j}^{'})$ ; thus $g_{j}^{'} < g_{σ (j)}^{'}$ and $x_{g_{j}^{'}} < x_{g_{σ (j)}^{'}}$ for every $j$ .

step 2.3step 3.2L1

5.1

In case (ii), $g^{'}$ is strictly increasing by [L3], so $(x_{g_{j}^{'}})$ is a subsequence of $(x_{k})$ , and it is increasing by [L4], so monotone.

step 4.3L3L4L5

6.1

Cases (i) and (ii) are literal negations of one another, so one of them holds; case (i) produces the monotone subsequence $(x_{g_{j}})$ and case (ii) the monotone subsequence $(x_{g_{j}^{'}})$ . Every sequence of reals therefore has a monotone subsequence.

step 4.1step 4.2step 5.1cases: exhaustive by negationcases-exhaustive∎

Remarks

The two cases are a negation pair, so no completeness is used to split them. Either peaks occur beyond every index, or they stop; nothing about $R$ enters the dichotomy. The only properties of the reals used anywhere above are trichotomy of the order, in step 3.2, and nothing else. In particular this lemma holds verbatim in any linearly ordered set, and it is A monotone sequence converges if and only if it is bounded, not this lemma, that consumes the least-upper-bound property inside Bolzano-Weierstrass: every bounded real sequence has a convergent subsequence.
Which kind of monotone subsequence is produced depends on the case, and the statement deliberately does not say which. Case (i) gives a nonincreasing subsequence and case (ii) a strictly increasing one. A sequence may satisfy case (i) with no increasing subsequence at all, for instance a constant sequence, so nothing stronger than "monotone" can be claimed uniformly.
Choice is not used. Both recursions choose a least element, supplied by the well-ordering principle (The well-ordering principle), so the functions $f$ and $h$ are defined outright rather than selected, and The recursion theorem then produces the index map. This is why the lemma, and with it Bolzano-Weierstrass in $R$ , needs no form of the axiom of choice, in contrast with the usual argument for sequential compactness in a general metric space.

Depends on

Used by

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

Dependency tree · two levels

30 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Bolzano-Weierstrass theorem (Wikipedia) (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed., §6.4 and §6.6 (standard reference, not scraped)
J. Lebl, Basic Analysis I, §2.3 (monotone subsequence) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 3 (standard reference, not scraped)
Peak Point Lemma (ProofWiki) (standard reference, not scraped)
The Monotone Subsequence Theorem (Mathonline) (standard reference, not scraped)