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 Cauchy-sequence reals have the least-upper-bound property
Statement
The Cauchy-sequence reals have the least-upper-bound property: every nonempty that is bounded above has a least upper bound . Hence, together with The reals form a totally ordered field, is a complete ordered field (Complete ordered field (least-upper-bound property)).
Facts & Assumptions
Given: A nonempty set bounded above by .
Upper bound, least upper bound, and the least-upper-bound property (Complete ordered field (least-upper-bound property)).
Every Cauchy sequence of reals converges to a real (The reals are complete).
Convergence and the Cauchy condition for real sequences are quantified over positive rational (Limits and Cauchy sequences of reals).
is Archimedean, so the reals are cofinal and (The Cauchy-sequence reals are Archimedean).
is a totally ordered field: midpoints , halving, and order arithmetic (The reals form a totally ordered field, Order on the reals).
The rationals embed densely; below any real lies a rational (The rationals embed densely in the reals).
Proof
Fix (possible as ); by [L6] choose a real , so is not an upper bound of , and put , an upper bound of .
Define by bisection: given (not an upper bound) and (an upper bound), let ; if is an upper bound set , otherwise set .
An induction on shows each is an upper bound of , each is not, , and .
Given rational , by [L4] choose with ; then for all , .
For both lie in the nested interval , so and likewise ; hence and are Cauchy sequences of reals.
By [L2], converges to a real and to a real . If , choose by [L6] a positive rational with . For all large , convergence and step 4.1 give , and , whence , a contradiction. If , choose ; for all large , and the two convergence bounds give , again a contradiction. Thus . For fixed and every , step 3.1 gives . If , choose and use ; if , choose and use . Each choice contradicts the displayed inequalities for all large , so .
Every satisfies for all , since each is an upper bound. If , choose by [L6] a positive rational with . Since , eventually , hence , contradicting . Therefore , so is an upper bound of .
If is any upper bound of , then for each some element of exceeds , because is not an upper bound; hence . If , choose by [L6] a positive rational with . Since , eventually , so , a contradiction. Thus , and is the least upper bound.
Hence exists in ; as was an arbitrary nonempty bounded-above set, has the least-upper-bound property and is a complete ordered field.
Depends on
Used by
- ℝ((t⁻¹)) does not have the least-upper-bound property; its canonical naturals have no supremum Corollary
- A complete domain is necessary for sequential uniform boundedness Counterexample
- An annihilating polynomial need not be minimal: √2 is a root of both x²-2 and x⁴-4 Counterexample
- The Koch curve is a uniform limit of polygonal paths of lengths (4/3)ⁿ but is not rectifiable Counterexample
- The unrestricted nested interval property fails in ℝ((t⁻¹)) Counterexample
- Real and imaginary parts, complex conjugation, and modulus Definition
- Riemannian distance on a connected manifold Definition
- The operator norm as the least bound and as the unit-sphere or unit-ball supremum Definition
- The sequence spaces c₀ and ell-infinity Definition
- Coordinate partial sums on c₀ Example
- ℚ(√2)≅ℚ[x]/(x²-2) with basis 1,√2 Example
- ℝ ≈ P(ℕ) in ZF, by the Cantor set for one injection and by the cuts {q ∈ ℚ : q < x} for the other; so | ℝ | = 2^ℵ₀ under the Axiom of Choice Example
- ℝ as a vector space over ℚ has a basis, and every such basis is infinite; the existence proof exhibits none Example
- ℝ with the half-open intervals [a,b) as a basis is not compact and, assuming the Axiom of Countable Choice, is Lindel"of, while its square is not Lindel"of, the antidiagonal being an uncountable closed discrete subspace Example
- The minimal polynomial of √2+√3 over ℚ is x⁴-4x²+1 Example
- The square roots of i are ±(1+i)/√2 Example
- Under choice, the Niemytzki plane is Tychonoff and locally metrizable but not normal, paracompact, or metrizable Example
- Canonical Banach complexification of a real Banach space Lemma
- Conjugation is an involutive real-field automorphism, zz̄=|z|², and modulus is definite, multiplicative, and subadditive Lemma
- Finite polygonal disk parametrizations and boundary surgery Lemma
- Free tail ultrafilters and bounded real ultralimit calculus Lemma
- Polygonal boundary crossing forces coverage by affine triangles Lemma
- Radial geodesics from one point reach every point under global exponential domain Lemma
- Triangle extrema and the tripod and branch rules for real trees Lemma
- Equivalence of the Cauchy and Dedekind constructions of ℝ Theorem
- Every complex number has a square root, by an explicit Cartesian formula Theorem
- Every infinite regular continued fraction converges to a unique real number Theorem
- For n at least one, open sets, closed sets, compact sets, open balls, boxes, rational open boxes, and rational half-open boxes generate the Borel sigma-algebra on Rⁿ Theorem
- Sequential uniform boundedness under countable choice Theorem
- Sylvester's law of inertia: every real symmetric form is congruent to diag(Iₚ,-I_q,0ᵣ), and (p,q,r) is unique Theorem
Dependency tree · two levels
24 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
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (standard reference, not scraped)
- T. Tao, Analysis I, 3rd ed., §6.4 (standard reference, not scraped)
- Purdue University notes: Number systems and the real numbers (standard reference, not scraped)
- East Tennessee State University notes: Uniqueness of the real numbers (standard reference, not scraped)