Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicableverified 2026-08-04 (gpt-5.6-sol-codex-subscription)
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 R‾=R∪{−∞,+∞}, 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

R‾:=R∪{−∞,+∞}.

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 R, and no operation of R (Complete ordered field (least-upper-bound property)) is redefined by anything below.

The order. For a,b∈R‾ declare

a≤b:⟺a=−∞  or  b=+∞  or  (a,b∈R and a≤b in R),

with R ordered as in Order on the reals, and write a<b for "a≤b and a≠b" as usual (Partial order and partially ordered set).

(R‾,≤) is a totally ordered set, and the inclusion of R preserves and reflects the order. All four checks are immediate from the displayed clauses.

  • Reflexive. For a=±∞ one of the first two clauses applies; for a∈R the third does, since a≤a in R.
  • Antisymmetric. Suppose a≤b and b≤a. If a=−∞ then b≤a forces b=−∞, since the clause a=+∞ fails and b,a are not both real. Symmetrically b=−∞ forces a=−∞, and a=+∞ or b=+∞ forces the other to be +∞. In the one remaining situation a and b are both real and antisymmetry is that of R.
  • Transitive. Let a≤b≤c. If a=−∞ or c=+∞ the conclusion is one of the first two clauses. Otherwise a≠−∞ forces, in a≤b, either b=+∞ or a,b∈R; and c≠+∞ forces, in b≤c, either b=−∞ or b,c∈R. The value b=+∞ is incompatible with the second alternative pair, so b is real, hence so are a and c, and transitivity is that of R.
  • Total. If a=−∞ or b=+∞ then a≤b; if b=−∞ or a=+∞ then b≤a; otherwise both are real and the order of R is total.
  • Preserved and reflected. For a,b∈R the first two clauses fail, so a≤b in R‾ says exactly a≤b in R.

In particular −∞ is the least and +∞ the greatest element of R‾, and −∞<x<+∞ for every x∈R.

Reflection. Extend negation by

−(+∞):=−∞,−(−∞):=+∞,

keeping the field negative on R. The resulting map ν:R‾→R‾, ν(a)=−a, satisfies ν(ν(a))=a and

a≤b  ⟺  −b≤−a(a,b∈R‾).

For a and b real this is the elementwise order reversal in R: translation invariance (Order is preserved by adding a constant and by adding inequalities) applied with the constant −a−b turns a<b into −b<−a and, applied with the constant a+b, turns it back, while a=b holds exactly when −a=−b. In every other case both sides are decided by the first two clauses of the order: a=−∞ makes both sides true, as does b=+∞, and if a≠−∞, b≠+∞ and a,b are not both real then one of a=+∞, b=−∞ holds and both sides are false.

Partial addition. For a,b∈R‾ the sum a+b is defined by

  • a+b = the field sum, when a,b∈R;
  • a+b:=+∞ when a=+∞ and b≠−∞, or b=+∞ and a≠−∞;
  • a+b:=−∞ when a=−∞ and b≠+∞, or b=−∞ and a≠+∞;

and the two sums (+∞)+(−∞) and (−∞)+(+∞) are left undefined. Addition is commutative where defined, and

−(a+b)=(−a)+(−b),

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 a,b∈R‾ the product ab is defined by

  • ab = the field product, when a,b∈R;
  • ab:=+∞ when one of a,b is ±∞, the other is ≠0, and both are >0 or both are <0;
  • ab:=−∞ when one of a,b is ±∞, the other is ≠0, and one is >0 and the other <0;

and every product with one factor 0 and the other ±∞ is left undefined. The comparisons >0 and <0 here are taken in the order above, under which +∞>0>−∞.

Nothing else is defined. There is no subtraction, no division, no exponentiation and no absolute value on R‾ 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

Depends on

Used by

…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