Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-06 (claude-sonnet-5)
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 monotone sequence converges if and only if it is bounded

Statement

Let (xk) be a monotone sequence of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences). Then (xk) converges if and only if it is bounded, that is if and only if there is M∈R with ∣xk∣≤M for every k∈N.

The forward implication holds for every sequence and is Every convergent sequence is bounded. What monotonicity buys is the converse, which is false for sequences in general.

Facts & Assumptions

Given: A monotone sequence (xk) of reals, with range S={xk:k∈N}.

[L2]

Monotone convergence: a nondecreasing sequence whose range is bounded above converges, to the supremum of its range; a nonincreasing sequence whose range is bounded below converges, to the infimum (A nondecreasing sequence bounded above converges to the supremum of its range, and a nonincreasing sequence bounded below to the infimum).

[L3]

Every convergent sequence of reals is bounded (Every convergent sequence is bounded).

[L4]

A sequence is bounded when some M satisfies ∣xk∣≤M for every k; its range is bounded above by u when xk≤u for every k, and bounded below by ℓ when ℓ≤xk for every k (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Lower bound, bounded below, bounded set).

[L5]

Absolute value: ∣t∣≤M exactly when −M≤t≤M (Basic properties of the absolute value).

Proof

technique · direct
1.1

Suppose (xk) converges. Then it is bounded by [L3], and this direction uses neither the monotonicity hypothesis nor any case distinction.

givenL3
1.2

Suppose instead that (xk) is bounded, and fix M with ∣xk∣≤M for every k; then −M≤xk≤M for every k, so the range S is bounded above by M and bounded below by −M.

givenL4L5assume-hyp
2.1

If (xk) is nondecreasing then its range is bounded above by step 1.2, so (xk) converges, to sup⁡S.

step 1.2L2assume-case nondec
2.2

If (xk) is nonincreasing then its range is bounded below by step 1.2, so (xk) converges, to inf⁡S.

step 1.2L2assume-case noninc
3.1

A monotone sequence is nondecreasing or nonincreasing, so those two cases exhaust the hypothesis, and in both a bounded monotone sequence converges.

step 2.1step 2.2L1cases: nondecreasing or nonincreasingcases-exhaustive
4.1

Both directions are established: a monotone sequence converges if and only if it is bounded.

step 1.1step 3.1∎

Remarks

Depends on

Used by

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