TheoremStatement: 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.

A nondecreasing sequence bounded above converges to the supremum of its range, and a nonincreasing sequence bounded below to the infimum

Statement

Let $(x_{k})$ be a sequence of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences) and let $S = {x_{k} : k \in N}$ be its range.

If $(x_{k})$ is nondecreasing (Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences) and $S$ is bounded above (Lower bound, bounded below, bounded set), then $(x_{k})$ converges (Limits and Cauchy sequences of reals) and $\lim_{k} x_{k} = \sup S .$
If $(x_{k})$ is nonincreasing and $S$ is bounded below, then $(x_{k})$ converges and $\lim_{k} x_{k} = \inf S .$

Both suprema and infima exist under the stated hypotheses: $S$ is nonempty, so the least-upper-bound property (Complete ordered field (least-upper-bound property)) supplies the first and Every nonempty set bounded below has an infimum the second, and each is unique (Suprema and infima are unique).

This is the first place in this track where the least-upper-bound property produces a limit. Everything on the sequences page held in any Archimedean ordered field; the theorem below does not, and the sequence of decimal truncations of $\sqrt{2}$ inside $Q$ is the standard witness of its failure there.

Facts & Assumptions

Given: A sequence $(x_{k})$ of reals with range $S = {x_{k} : k \in N}$ , which is nonempty since $x_{0} \in S$ .

[L1]

Least-upper-bound property and uniqueness: a nonempty subset of $R$ that is bounded above has a unique supremum, which is an upper bound of it (Complete ordered field (least-upper-bound property), Suprema and infima are unique).

[L2]

Greatest-lower-bound property and uniqueness: a nonempty subset of $R$ that is bounded below has a unique infimum, which is a lower bound of it (Every nonempty set bounded below has an infimum, Suprema and infima are unique).

[L3]

Epsilon characterisation of the supremum: if $u$ is an upper bound of a nonempty $S$ , then $u = \sup S$ exactly when for every $ε > 0$ there is $s \in S$ with $u - ε < s$ (Epsilon characterisation of the supremum).

[L4]

Epsilon characterisation of the infimum: if $ℓ$ is a lower bound of a nonempty $T$ , then $ℓ = \inf T$ exactly when for every $ε > 0$ there is $t \in T$ with $t < ℓ + ε$ (Epsilon characterisation of the infimum).

[L5]

Monotonicity: nondecreasing means $x_{j} \leq x_{k}$ whenever $j \leq k$ , and nonincreasing means $x_{j} \geq x_{k}$ whenever $j \leq k$ (Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences).

[L6]

Convergence, tested against a real $ε$ : $(x_{k})$ converges to $x$ when for every rational $ε > 0$ there is $K$ with $∣ x_{k} - x ∣ < ε$ for all $k \geq K$ , and producing such a $K$ for every real $ε > 0$ establishes this, since every positive rational is a positive real (Limits and Cauchy sequences of reals, Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L7]

Absolute value: for $c > 0$ , $∣ t ∣ < c$ exactly when $- c < t < c$ (Basic properties of the absolute value).

[L8]

Bounded above and bounded below, for a subset of $R$ (Lower bound, bounded below, bounded set).

Proof

technique · direct

1.1

Assume $(x_{k})$ is nondecreasing and $S$ is bounded above. Since $S$ is nonempty, $u : = \sup S$ exists, is unique, and is an upper bound of $S$ .

givenL1L8

1.2

Assume $(y_{k})$ is nonincreasing with range $T$ bounded below. Since $T$ is nonempty, $ℓ : = \inf T$ exists, is unique, and is a lower bound of $T$ .

givenL2L8

2.1

Every term satisfies $x_{k} \leq u$ , because $x_{k} \in S$ and $u$ is an upper bound of $S$ .

step 1.1L1

2.2

Every term satisfies $ℓ \leq y_{k}$ , because $y_{k} \in T$ and $ℓ$ is a lower bound of $T$ .

step 1.2L2

2.3

Let $ε > 0$ be an arbitrary real. By [L3] there is $s \in S$ with $u - ε < s$ , and every element of $S$ is a term, so $s = x_{K}$ for some $K \in N$ .

step 1.1L3choose

2.4

Let $ε > 0$ be an arbitrary real. By [L4] there is $t \in T$ with $t < ℓ + ε$ , and $t = y_{L}$ for some $L \in N$ .

step 1.2L4choose

3.1

For every $k \geq K$ we have $x_{K} \leq x_{k}$ by monotonicity, hence $u - ε < x_{K} \leq x_{k}$ .

step 2.3L5

3.2

For every $k \geq L$ we have $y_{k} \leq y_{L}$ by monotonicity, hence $y_{k} \leq y_{L} < ℓ + ε$ .

step 2.4L5

4.1

For every $k \geq K$ : subtracting $u$ from $u - ε < x_{k} \leq u$ gives $- ε < x_{k} - u \leq 0 < ε$ , so $∣ x_{k} - u ∣ < ε$ .

step 2.1step 3.1L7algebra

4.2

For every $k \geq L$ : subtracting $ℓ$ from $ℓ \leq y_{k} < ℓ + ε$ gives $- ε < 0 \leq y_{k} - ℓ < ε$ , so $∣ y_{k} - ℓ ∣ < ε$ .

step 2.2step 3.2L7algebra

5.1

The real $ε > 0$ was arbitrary and $K$ was produced from it, so $(x_{k})$ converges to $u = \sup S$ , which is claim 1.

step 4.1L6

5.2

The real $ε > 0$ was arbitrary and $L$ was produced from it, so $(y_{k})$ converges to $ℓ = \inf T$ , which is claim 2.

step 4.2L6

6.1

Both claims are established, so a nondecreasing sequence bounded above converges to the supremum of its range and a nonincreasing sequence bounded below converges to the infimum of its range.

step 5.1step 5.2∎

Remarks

Only one half is proved twice. Claim 2 could instead be deduced from claim 1 by reflection, since $(- y_{k})$ is nondecreasing and bounded above and $\inf T = - \sup (- T)$ (Every nonempty set bounded below has an infimum). The direct argument is written out because it is no longer, and because it puts Epsilon characterisation of the infimum to work in the place it was proved for, rather than routing an infimum statement through a supremum statement and a sign change.
The limit is the supremum of the range, not merely some upper bound. That identification is what Epsilon characterisation of the supremum supplies and it is the useful part of the theorem: it is how a limit is computed from a monotone construction, as in the recursive sequences of the examples page, rather than merely shown to exist.
Boundedness on the other side is automatic and is not a hypothesis. A nondecreasing sequence is bounded below by $x_{0}$ (Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences), so "nondecreasing and bounded above" already means "nondecreasing and bounded"; this is what makes A monotone sequence converges if and only if it is bounded an equivalence rather than a one-sided statement.
Without the hypothesis of boundedness the conclusion fails completely, and fails in a describable way: a nondecreasing sequence that is not bounded above diverges to $+ \infty$ (A nondecreasing sequence that is not bounded above diverges to $+ \infty$ ), so a nondecreasing sequence either converges to the supremum of its range or runs away, with no third possibility.

Depends on

Used by

Dependency tree · two levels

27 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

Monotone convergence theorem (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 3 (Thm 3.14) (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed., §6.3 (Prop. 6.3.8) (standard reference, not scraped)
J. Lebl, Basic Analysis I, §2.2 (Thm 2.2.5) (standard reference, not scraped)