A real number is an element of the unique complete ordered field which contains the rational numbers.
A field is a triple , where
is a commutative group with the identity element .
is a commutative monoid with the identity element .
is a commutative group.
Examples of fields include rational numbers, real numbers, complex numbers, and finite fields.
An ordered field is a tuple , where
is a field.
is a total order relation in .
Examples of ordered fields include rational numbers and real numbers.
An affinely extended ordered field is a tuple , where
and are called minus-infinity and plus-infinity, respectively.
is an ordered field.
Such an extended field is not a field. For example, the infinities do not have an inverse element. Most often the significance of the infinities is that they allow for compact notation, as used for infinite real intervals and unbounded limiting behaviour of functions.
The Real concept abstracts elements of an affinely extended ordered field.
Specifically, by this abstraction we aim to capture implementations of
floating point numbers and exact rational numbers. The intent is to be able
to use the same algorithms independent of the representation of numbers.
For example, the same geometric algorithms may be used with either floating
point arithmetic or exact rational arithmetic.