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.
The five completeness properties of an ordered field: least upper bound, monotone convergence, nested intervals, Bolzano-Weierstrass, and Cauchy completeness
Definition
Throughout, is an ordered field (Ordered field) with its order and its absolute value. Sequences in , and the notions of convergence in , Cauchyness in , boundedness, nondecreasing and nonincreasing, subsequence, closed interval , nesting, and lengths tending to in , are the ones fixed once and for all in Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field. They are not restated here and they are never read in : every below ranges over the positive elements of itself.
A sequence in is bounded above when there is with for every , and a subset is bounded above when there is with for every (Complete ordered field (least-upper-bound property), Upper bound, least upper bound, and strict upper bound).
The following are five properties that may or may not have.
-
(LUB), the least-upper-bound property. Every nonempty that is bounded above has a least upper bound in . This is exactly the condition that makes a complete ordered field (Complete ordered field (least-upper-bound property)), and the two names are used interchangeably here.
-
(MCT), the monotone convergence property. Every nondecreasing sequence in that is bounded above converges in .
-
(NIP), the nested interval property. For every nested sequence of closed intervals of whose lengths tend to in , the intersection
is nonempty.
-
(BW), the Bolzano-Weierstrass property. Every bounded sequence in has a subsequence that converges in .
-
(CC), Cauchy completeness. Every Cauchy sequence in converges in .
Alongside these we use the Archimedean property (ARCH) of Archimedean ordered field: for every there is a natural number with .
Remarks
-
(NIP) is stated in the shrinking form because that is the form both satisfied by the formal Laurent series field and used by the bisection theorem. The field is Cauchy complete without having least upper bounds (Every Cauchy sequence in converges: is sequentially Cauchy complete, does not have the least-upper-bound property; its canonical naturals have no supremum), and it satisfies shrinking (NIP) ( has the nested interval property for lengths tending to ). The same shrinking condition is exactly what the bisection argument of Nested intervals plus the Archimedean property imply Bolzano-Weierstrass, by repeated bisection produces.
-
"Lengths tend to " is read in . For a non-Archimedean this is strictly stronger than the same words read in through some identification of the rational scalars, and the difference is not academic: the remarks of has the nested interval property for lengths tending to exhibit intervals in whose lengths are the real constants , which tend to in the ordinary real sense and do not tend to in the order of that field.
-
Boundedness of a sequence is two-sided, boundedness above is not. Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field calls bounded when for every , which is the hypothesis of (BW); (MCT) asks only for the one-sided bound , which for a nondecreasing sequence is the only side in question, since always.
-
(MCT) is stated for nondecreasing sequences only. The nonincreasing case is not a separate assumption: if is nonincreasing and bounded below by then is nondecreasing and bounded above by , and exactly when , because . That reduction is used in the proof of The monotone convergence property plus the Archimedean property imply the least-upper-bound property.
-
Nothing here presumes that any of the five holds. They are predicates on an ordered field, and the point of the page they open is that in the presence of (ARCH) they are all the same predicate (For an ordered field the five completeness properties are equivalent, provided the Archimedean property is assumed alongside nested intervals and Cauchy completeness), while without it two of them are strictly weaker (FALSE: the nested interval property alone implies the least-upper-bound property, FALSE: an ordered field in which every Cauchy sequence converges has the least-upper-bound property).
-
(CC) is this library's third rendering of "Cauchy complete", and for all three agree. Cauchy sequence in a metric space and Complete metric space: every Cauchy sequence converges in the space read Cauchyness and completeness in a metric space, and the case of and for with the Euclidean metric are complete, componentwise from the Cauchy criterion in proves complete; Limits and Cauchy sequences of reals reads both notions for real sequences, with ranging over the positive rationals; the present definition reads them in an ordered field . For under the metric of The absolute value makes a metric space: is a metric, its open balls are the intervals , and it is unbounded the three unfold to the same quantified statement: below every positive real lies a positive rational (The rationals embed densely in the reals), so the two ranges of pick out the same Cauchy sequences and the same convergent ones. So " satisfies (CC)" is a statement this library has already proved twice, as The Cauchy criterion from the least-upper-bound property: in a complete ordered field every Cauchy sequence converges and as the case of and for with the Euclidean metric are complete, componentwise from the Cauchy criterion in . The parallel stops at . The absolute value of an ordered field takes its values in , while a metric is required to take its values in (Metric space: iff , symmetry, and the triangle inequality; pseudometric and ultrametric), so for a non-Archimedean the map is not a metric in this library's sense and the metric development says nothing about it. That is why Sequence basics in an arbitrary ordered field: limits are unique, limits preserve non-strict inequalities, convergent sequences are Cauchy, Cauchy sequences are bounded, and a Cauchy sequence with a convergent subsequence converges had to be proved from the order axioms alone, although its Cauchy clauses reappear for metric spaces as Every convergent sequence in a metric space is Cauchy, Every Cauchy sequence in a metric space is bounded and A Cauchy sequence in a metric space with a convergent subsequence converges to that subsequence’s limit. Neither development generalises the other; the comparison above identifies their agreement at without claiming that is their only overlap.
Depends on
Used by
- On a closed interval of ℚ there is a continuous unbounded function, a bounded one with no maximum, and one without the intermediate value property Counterexample
- Over ℚ there is a nonconstant differentiable function with identically zero derivative, so Rolle and the mean value theorem both fail Counterexample
- ℝ((t⁻¹)), the formal Laurent series field, is Cauchy complete, non-Archimedean, and lacks the least-upper-bound property Example
- FALSE: an ordered field in which every Cauchy sequence converges has the least-upper-bound property False statement
- FALSE: the nested interval property alone implies the least-upper-bound property False statement
- An ordered field with the least-upper-bound property has the nested interval property and is Archimedean Lemma
- Bolzano-Weierstrass alone forces the Archimedean property, so it needs no separate Archimedean hypothesis Lemma
- Bolzano-Weierstrass implies Cauchy completeness in any ordered field Lemma
- Cauchy completeness plus the Archimedean property imply the monotone convergence property Lemma
- Nested intervals plus the Archimedean property imply Bolzano-Weierstrass, by repeated bisection Lemma
- The monotone convergence property alone forces the Archimedean property, so it carries no separate Archimedean hypothesis Lemma
- The monotone convergence property plus the Archimedean property imply the least-upper-bound property Lemma
- Which of the five completeness properties carry the Archimedean property on their own, and which must be handed it Remark
- For an ordered field the five completeness properties are equivalent, provided the Archimedean property is assumed alongside nested intervals and Cauchy completeness Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 34 results over 9 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- J. F. Hall, Completeness of Ordered Fields (standard reference, not scraped)
- Completeness of the real numbers (Wikipedia) (standard reference, not scraped)
- Least-upper-bound property (Wikipedia) (standard reference, not scraped)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 and Ch. 3 (standard reference, not scraped)
- J. Lebl, Basic Analysis I, §1.2 and §2.3 (standard reference, not scraped)