Alphabeta MathHow 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.
The Cauchy criterion from the least-upper-bound property: in a complete ordered field every Cauchy sequence converges
Statement
Every Cauchy sequence of reals converges to a real (Limits and Cauchy sequences of reals).
More carefully, this is a statement about the axioms: in a complete ordered field, that is in an ordered field with the least-upper-bound property (Complete ordered field (least-upper-bound property)), every Cauchy sequence converges. The proof below uses nothing about except that property, through Bolzano-Weierstrass: every bounded real sequence has a convergent subsequence.
This library already knows the conclusion by a different route. It is proved on the Cauchy-construction page, where is built out of Cauchy sequences of rationals and completeness is read off the construction. That proof is about a particular construction; this one is about the axioms, and it is what tells us the statement holds in any complete ordered field, however it was obtained.
Facts & Assumptions
Given: A Cauchy sequence of reals, being a complete ordered field.
Every Cauchy sequence of reals is bounded (Every Cauchy sequence of reals is bounded).
Bolzano-Weierstrass: every bounded sequence of reals has a convergent subsequence, that is a strictly increasing and a real with (Bolzano-Weierstrass: every bounded real sequence has a convergent subsequence).
A Cauchy sequence with a subsequence converging to converges to (A Cauchy sequence with a convergent subsequence converges, to that subsequence’s limit).
Convergence of a sequence of reals to a real (Limits and Cauchy sequences of reals).
is a complete ordered field, and this is the only property of it used, through [L2] (Complete ordered field (least-upper-bound property)).
Proof
The Cauchy sequence is bounded.
Being bounded, has a convergent subsequence: fix a strictly increasing and a real with .
The sequence is Cauchy and has a subsequence converging to , so it converges to .
An arbitrary Cauchy sequence of reals has therefore been shown to converge to a real, so every Cauchy sequence of reals converges, and this was derived from the least-upper-bound property alone.
Remarks
-
The three steps are exactly the three lemmas, and each is sharp. A Cauchy sequence is bounded (Every Cauchy sequence of reals is bounded); a bounded sequence has a convergent subsequence (Bolzano-Weierstrass: every bounded real sequence has a convergent subsequence); a Cauchy sequence with a convergent subsequence converges (A Cauchy sequence with a convergent subsequence converges, to that subsequence’s limit). Dropping the Cauchy hypothesis at the last step breaks the chain, since a bounded sequence need not converge (FALSE: every bounded sequence converges).
-
Where completeness enters. Only in the middle step, and there only through A monotone sequence converges if and only if it is bounded inside the proof of Bolzano-Weierstrass. The first and third steps hold in any ordered field. That localisation is the reason for the page order.
-
The converse needs an extra hypothesis. Cauchy completeness alone does not imply the least-upper-bound property; it does so together with the Archimedean property, and there are Cauchy complete non-Archimedean ordered fields that are not Dedekind complete. This library does not prove that here; the equivalences between the forms of completeness are the subject of a later page, and Two independent proofs that is Cauchy complete, and why the library records both states precisely what is and is not established now.
-
The name. "Cauchy criterion" is the useful reading: the theorem lets one prove convergence without producing the limit, which is what makes it the standard tool for series and for uniform convergence later on.
-
The construction-side proof of the same sentence is The reals are complete, and Two independent proofs that is Cauchy complete, and why the library records both sets out why this library keeps both. Neither proof uses the other, and nothing above depends on that item.
Depends on
Used by
- The truncated decimal approximations of √2 form a Cauchy sequence of rationals with no rational limit Counterexample
- The bounded real-valued functions on a set, with the supremum metric, form a complete metric space Example
- FALSE: every Cauchy sequence in a metric space converges False statement
- Complete metrizability: admitting a topologically equivalent complete metric is preserved by homeomorphism and by closed subspaces, and (0,∞) has it without being complete Lemma
- Two independent proofs that ℝ is Cauchy complete, and why the library records both Remark
- A continuous integrand is Riemann–Stieltjes integrable against every bounded-variation integrator Theorem
- A sequence of real-valued functions converges uniformly if and only if it is uniformly Cauchy Theorem
- A series converges iff for every ε > 0 there is N with |aₘ₊₁ + … + aₙ| < ε for all n > m ≥ N Theorem
- Cauchy criterion for improper integrals Theorem
- Every contractive sequence is Cauchy, hence converges, with error bound |x - xₖ| ≤ cᵏ⁻¹|x₂ - x₁|/(1-c) for k ≥ 1 Theorem
- Every metric space has a completion, constructed as the equivalence classes of its Cauchy sequences Theorem
- Linearity and interval additivity of the Riemann–Stieltjes integral Theorem
- ℝ and ℝⁿ for n ≥ 1 with the Euclidean metric are complete, componentwise from the Cauchy criterion in ℝ Theorem
- The Cauchy criterion for a Henstock–Kurzweil integral at a missing endpoint Theorem
- Two bounded-variation functions with no common discontinuity are Riemann–Stieltjes integrable Theorem
- Young's Riemann–Stieltjes existence theorem for rational Hölder exponents Theorem
Dependency tree · two levels
20 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
- Completeness of the real numbers (Wikipedia) (standard reference, not scraped)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 3 (Thm 3.11(c)) (standard reference, not scraped)
- T. Tao, Analysis I, 3rd ed., §6.4 (Thm 6.4.18) (standard reference, not scraped)
- J. Lebl, Basic Analysis I, §2.4 (Thm 2.4.5) (standard reference, not scraped)