The reals form a totally ordered field

Depends on

• Order on the reals
• The real numbers
• The reals form a field
• A non-null Cauchy sequence is eventually bounded away from zero, with constant sign
• The rationals form a totally ordered field
• Null sequence

Used by

• Certified complex-polynomial root isolation in exact algebraic arithmetic Algorithm
• A nonnegative measurable function with finite integral is finite almost everywhere Corollary
• ℝ((t⁻¹)) does not have the least-upper-bound property; its canonical naturals have no supremum Corollary
• The Cauchy-sequence reals have the least-upper-bound property Corollary
• The symmetric Lovász Local Lemma under ep(d+1)≤1 Corollary
• A full-rank local Hessian does not capture both posterior modes Counterexample
• Adjoining one root need not split the polynomial: ℚ(³√2) does not split x³-2 Counterexample
• Bezout needs algebraic closure: an imaginary conic has no real point Counterexample
• Not every ordered field is Archimedean Counterexample
• The first quadrant of ℝ² contains 0 and is closed under addition and is not a linear subspace, since it is not closed under multiplication by -1 Counterexample
• The integers do not have property (T) Counterexample
• The unrestricted nested interval property fails in ℝ((t⁻¹)) Counterexample
• Acceptance polynomials and approximate degree on Boolean domains Definition
• Algebraically constructible real numbers as the smallest real subfield closed under positive square roots Definition
• Cardinal-polynomial interpolation Definition
• Finite probability spaces, outcome weights, events, and event probabilities Definition
• Finite type-II testing function with explicit orientation Definition
• For n≥1, the determinant over a commutative ring by the Leibniz formula, and |det A| for a real matrix Definition
• Orientation of a finite-dimensional real vector space Definition
• Positive and negative definiteness, the inertia (p,q,r), rank p+q, and signature p-q of a real symmetric bilinear or quadratic form Definition
• Real edge-weighted graphs, total tree weight and minimum spanning trees Definition
• Test size and power Definition
• The formal Laurent series ℝ((t⁻¹)): support bounded below, valuation, leading coefficient Definition
• The real Coxeter form, its radical, reflections, and form-preserving maps Definition
• The uniform probability space on a nonempty finite set Definition
• Variance, standard deviation, and covariance on a finite probability space Definition
• A lighter-tailed proposal has no finite rejection envelope Example
• A null normal admits no reflection of the displayed form Example
• A polynomial-tail law with finite variance Example
• Assuming Choice, real algebraic numbers embed properly in an algebraic closure of ℚ Example
• Assuming the Axiom of Choice, compactness of [0,1] derived from the subbase lemma alone, using only the rays as a subbasis and the least upper bound property Example
• One corrupted block is rejected by the geometric median Example
• Positive type on a discrete group: the identity mass, characters, and the regular GNS model Example
• Property (T) for finite groups via normalized counting measure Example
• ℚ and ℝ are fields, hence commutative rings, integral domains and ordered rings, all of characteristic 0 Example
• ℚ(√2) carries exactly two distinct field orders, exchanged by the conjugation √2 ↦ -√2 Example
• ℚ(³√2) has three embeddings into ℚ̄ but only one ℚ-automorphism 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
• ℝ is a vector space over itself, over the embedded copy of ℚ by restriction of scalars, and over ℚ itself via the embedding Example

…and 66 more results.

Cited to discharge well-definedness by Order on the reals.

Dependency tree · two levels

16 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

• T. Tao, Analysis I, 3rd ed., §5.4 (standard reference, not scraped)
• W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (standard reference, not scraped)
• L. S. Krapp, Constructions of the real numbers: a set theoretical approach (Oxford, 2014) (standard reference, not scraped)