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 extended real line , its order, and the arithmetic that is left undefined
Definition
Fix two objects and , distinct from one another and neither of them a real number (The real numbers), and set
This is a new object, introduced here explicitly with its own order and its own partial arithmetic. It is not an enlargement of the field , and no operation of (Complete ordered field (least-upper-bound property)) is redefined by anything below.
The order. For declare
with ordered as in Order on the reals, and write for " and " as usual (Partial order and partially ordered set).
is a totally ordered set, and the inclusion of preserves and reflects the order. All four checks are immediate from the displayed clauses.
- Reflexive. For one of the first two clauses applies; for the third does, since in .
- Antisymmetric. Suppose and . If then forces , since the clause fails and are not both real. Symmetrically forces , and or forces the other to be . In the one remaining situation and are both real and antisymmetry is that of .
- Transitive. Let . If or the conclusion is one of the first two clauses. Otherwise forces, in , either or ; and forces, in , either or . The value is incompatible with the second alternative pair, so is real, hence so are and , and transitivity is that of .
- Total. If or then ; if or then ; otherwise both are real and the order of is total.
- Preserved and reflected. For the first two clauses fail, so in says exactly in .
In particular is the least and the greatest element of , and for every .
Reflection. Extend negation by
keeping the field negative on . The resulting map , , satisfies and
For and real this is the elementwise order reversal in : translation invariance (Order is preserved by adding a constant and by adding inequalities) applied with the constant turns into and, applied with the constant , turns it back, while holds exactly when . In every other case both sides are decided by the first two clauses of the order: makes both sides true, as does , and if , and are not both real then one of , holds and both sides are false.
Partial addition. For the sum is defined by
- = the field sum, when ;
- when and , or and ;
- when and , or and ;
and the two sums and are left undefined. Addition is commutative where defined, and
each side being defined exactly when the other is: the excluded pairs are exchanged by , and the three clauses above are exchanged accordingly.
Partial multiplication. For the product is defined by
- = the field product, when ;
- when one of is , the other is , and both are or both are ;
- when one of is , the other is , and one is and the other ;
and every product with one factor and the other is left undefined. The comparisons and here are taken in the order above, under which .
Nothing else is defined. There is no subtraction, no division, no exponentiation and no absolute value on in this library; where such an expression is wanted it is written out in the two defined operations, and where a case falls in the undefined list the statement carries an explicit hypothesis saying so.
Remarks
-
is not a field, and not an ordered field. It has no additive inverse for : is whenever it is defined and is never . So none of the field axioms (Complete ordered field (least-upper-bound property)) is available here, and no algebraic manipulation valid in may be transported to without a separate justification.
-
Why the excluded cases are excluded. The three defined clauses of each operation are exactly the cases in which the value is forced by the limiting behaviour of the sequences involved, and the excluded cases are exactly the ones in which it is not. For the product this is proved on the companion page: Null times divergent has no rule: with gives product limit , and with gives divergence ↗ exhibits a null sequence and two sequences diverging to whose products behave differently, so no value assigned to could be compatible with products of limits. The same phenomenon rules out a value for : with and the sum is constantly , while with it diverges to . Leaving them undefined is not squeamishness, it is the only option that keeps every later statement about limits true without a side condition hidden inside the arithmetic.
-
This is the separate introduction that Conventions: , unbounded sets, and the extended reals points to. That remark refuses the conventions and inside , and records that the extended real line is introduced explicitly here, with its own order and its own partial arithmetic kept separate from rather than quietly extending it. This is that introduction. The suprema and infima of Complete ordered field (least-upper-bound property), Greatest lower bound (infimum) and the whole suprema page remain real numbers with their nonempty and bounded hypotheses intact; what is new is a separate supremum operation, taken in and named as such, supplied by Every subset of has a least upper bound and a greatest lower bound in , agreeing with the real supremum and infimum on nonempty sets bounded in .
-
The symbols were already in circulation, and this definition does not change what they meant. Divergence to and to defines the single phrase "" as an abbreviation for a condition on , and says in as many words that it does not define an object named . That reading is still correct: nothing in Divergence to and to is restated or reinterpreted here, and Convergence in and the extended subsequential limit set: is an extended subsequential limit when some subsequence converges to , or diverges to is where the two are related, by a definition that quotes the old one rather than replacing it. Likewise the interval notation of Intervals of : the nine order-convex forms, nondegeneracy, and length is notation for a condition on one side, not an endpoint, and stays that way.
-
Why the order is defined by three clauses rather than by a picture. The clauses are what the verifications above actually use, and they make the two facts that later proofs lean on immediate: every element is and every element is , with no case analysis at the point of use.
Depends on
Used by
- Kummer with ζₖ = 1 recovers the ratio test Corollary
- Raabe is Kummer with ζₖ = k+1: for positive terms, liminf (k+1)(aₖ/aₖ₊₁ - 1) > 1 gives convergence and limsup < 1 gives divergence Corollary
- The limit inferior is the least subsequential limit in ℝ̄ Corollary
- Whenever the ratio test decides, the root test decides the same way, and the converse fails Corollary
- A sequence with limsup = +∞: the greatest subsequential limit exists only in ℝ̄ Counterexample
- Null times divergent has no rule: xₖ = 1/k with yₖ = ck gives product limit c, and with yₖ = k² gives divergence Counterexample
- xₖ = (-1)ᵏ, yₖ = (-1)ᵏ⁺¹ give limsup(xₖ + yₖ) = 0 < 2 = limsup xₖ + limsup yₖ Counterexample
- xₖ = 1 + (-1)ᵏ, yₖ = 1 + (-1)ᵏ⁺¹ give limsup(xₖ yₖ) = 0 < 4 Counterexample
- A real power series about a centre, its interval of convergence, and its radius in [0,+∞] Definition
- A signed measure is countably additive and takes at most one infinite value Definition
- Convergence in ℝ̄ and the extended subsequential limit set: L ∈ ℝ̄ is an extended subsequential limit when some subsequence converges to L, or diverges to L = ±∞ Definition
- Counting measure on an arbitrary set Definition
- Extended diameter for Hausdorff covers Definition
- Extended-real-valued measurable functions Definition
- Finitely additive nonnegative set functions Definition
- For bounded f on [a,b] and a partition P: the infimum mᵢ and supremum Mᵢ of f on the i-th subinterval, and the lower and upper Darboux sums L(f,P) = ∑ᵢ mᵢ Δᵢ and U(f,P) = ∑ᵢ Mᵢ Δᵢ Definition
- Half-open boxes in ℝⁿ and their volume Definition
- Improper multiple integrals and absolute convergence on open sets Definition
- Injectivity radius at a point and of a manifold Definition
- Limit superior and limit inferior of a nonnegative extended-real sequence Definition
- Limit superior and limit inferior of a real sequence as infₙ sup_k ≥ n xₖ and supₙ inf_k ≥ n xₖ in ℝ̄ Definition
- Measures on sigma-algebras Definition
- Oscillation of a real function on subsets of ℝᵐ and at a point Definition
- Outer measures Definition
- Paths in ℝⁿ, inscribed polygonal sums, arc length as their supremum, and rectifiability Definition
- Premeasures on algebras of sets Definition
- Series in the nonnegative extended real line Definition
- Square-summable families on an arbitrary index set and the space ℓ²(I) Definition
- The Borel sigma-algebra on the extended real line Definition
- The convergence and absolute-convergence abscissae of a Dirichlet series Definition
- The equal-radius polydisc boundary function Definition
- The four Dini derivatives of a real function at a point Definition
- The order of a zero of a holomorphic function Definition
- The oscillation ω_f(S) = sup{ |f(x) - f(y)| : x, y ∈ S } of f on a set and the oscillation ω_f(c) = inf_δ > 0 ω_f(A ∩ N_δ(c)) at a point, both taken in the extended reals Definition
- The positive and negative parts of a function Definition
- The total variation |nu|(E) from countable measurable partitions Definition
- (-1)ᵏ has liminf = -1 and limsup = 1, so it does not converge Example
- A positive sequence making all three inequalities of the ratio-to-root chain strict Example
- A series with ratio limit exactly 1 that Raabe decides Example
- aₖ = 2^-k + (-1)ᵏ has liminf aₖ₊₁/aₖ = 1/8, limsup aₖ₊₁/aₖ = 2 and lim aₖ^1/k = 1/2 Example
…and 43 more results.
Dependency tree · two levels
15 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
- Extended real number line (Wikipedia) (standard reference, not scraped)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (1.23, the extended real number system) (standard reference, not scraped)
- T. Tao, Analysis I, 3rd ed., §6.2 (the extended real number system) (standard reference, not scraped)
- J. K. Hunter, Measure Theory notes (standard reference, not scraped)