Alphabeta Math

Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness

About this page
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.

✓ 15 results · all verified · 13 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 2 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.
1 · Prerequisites
Real Analysis
Set Theory
2 · Logical flowchart

3 · Items

Definition

Intervals of ℝ: the nine order-convex forms, nondegeneracy, and length

Definition

Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences

Theorem

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

Lemma

A nondecreasing sequence that is not bounded above diverges to +∞

Corollary

A monotone sequence converges if and only if it is bounded

Theorem

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

Definition

Subsequential limit of a real sequence, and the subsequential limit set

Lemma

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

Theorem

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

Lemma

Every Cauchy sequence of reals is bounded

Lemma

A Cauchy sequence with a convergent subsequence converges, to that subsequence’s limit

Theorem

The Cauchy criterion from the least-upper-bound property: in a complete ordered field every Cauchy sequence converges

Lemma

For |r| < 1 the sequence rᵏ is null, and for |r| > 1 the sequence |r|ᵏ diverges to +∞

Definition

Contractive sequence: |xₖ₊₂ - xₖ₊₁| ≤ c |xₖ₊₁ - xₖ| for a fixed 0 < c < 1

Theorem

Every contractive sequence is Cauchy, hence converges, with error bound |x - xₖ| ≤ cᵏ⁻¹|x₂ - x₁|/(1-c) for k ≥ 1

Lemma

The even and odd index maps and the alternating sequence: strictly increasing e, o with ℕ their disjoint union, and the unique (sₖ) with s₀ = 1, s_σ(k) = -sₖ, which satisfies |sₖ| = 1, s ∘ e ≡ 1 and s ∘ o ≡ -1

Remark

Two independent proofs that ℝ is Cauchy complete, and why the library records both

False statement

FALSE: a nested sequence of nonempty bounded open intervals has nonempty intersection

False statement

FALSE: if |xₖ₊₁ - xₖ| → 0 then (xₖ) is Cauchy

False statement

FALSE: a sequence with a convergent subsequence is bounded (the converse of Bolzano-Weierstrass)

Sources