nLab Archimedean ordered field




An Archimedean ordered field is an ordered field that satisfies the archimedean property.


The rational numbers are the initial ordered field, so for every ordered field FF there is a field homomorphism h:Fh:\mathbb{Q}\to F. FF is Archimedean if for all elements aFa\in F and bFb\in F, if a<ba \lt b, then there exists a rational number qq\in \mathbb{Q} such that a<h(q)a \lt h(q) and h(q)<bh(q) \lt b.


Every Archimedean ordered field is a dense linear order. This means that the Dedekind completion of every Archimedean ordered field is the field of real numbers.

Every Archimedean ordered field is a differentiable space:

Pointwise continuous functions

Let FF be an Archimedean ordered field. A function f:FFf:F \to F is continuous at a point cFc \in F if

isContinuousAt(f,c)ϵ(0,).xF.δ(0,).(|xc|<δ)(|f(x)f(c)|<ϵ)isContinuousAt(f, c) \coloneqq \forall \epsilon \in (0, \infty). \forall x \in F. \exists \delta \in (0, \infty). (\vert x - c \vert \lt \delta) \implies (\vert f(x) - f(c) \vert \lt \epsilon)

ff is pointwise continuous in FF if it is continuous at all points cc:

isPointwiseContinuous(f)cF.isContinuousAt(f,c)isPointwiseContinuous(f) \coloneqq \forall c \in F. isContinuousAt(f, c)

The set of all pointwise continuous functions is defined as

C 0(F){fFF|isPointwiseContinuous(f)}C^0(F) \coloneqq \{f \in F \to F \vert isPointwiseContinuous(f)\}

Pointwise differentiable functions

Let FF be an Archimedean ordered field. A function f:FFf:F \to F is differentiable at a point cFc \in F if

isDifferentiableAt(f,c)isContinuousAt(f,c)×LF.ϵ(0,).xF.δ(0,).h(δ,0)(0,δ).|f(c+h)f(c)hL|<ϵisDifferentiableAt(f, c) \coloneqq isContinuousAt(f, c) \times \exists L \in F. \forall \epsilon \in (0, \infty). \forall x \in F. \exists \delta \in (0, \infty). \forall h \in (-\delta, 0) \cup (0, \delta). \left| \frac{f(c + h) - f(c)}{h} - L \right| \lt \epsilon

ff is pointwise differentiable in FF if it is differentiable at all points cc:

isPointwiseDifferentiable(f)cF.isDifferentiableAt(f,c)isPointwiseDifferentiable(f) \coloneqq \forall c \in F. isDifferentiableAt(f, c)

The set of all pointwise differentiable functions is defined as

D 0(F){fFF|isPointwiseDifferentiable(f)}D^0(F) \coloneqq \{f \in F \to F \vert isPointwiseDifferentiable(f)\}


Archimedean ordered fields include

Non-Archimedean ordered fields include


The definition of the Archimedean property for an ordered field is given in section 4.3 of

  • Auke B. Booij, Analysis in univalent type theory (2020) [[etheses:10411, pdf]]

Last revised on January 12, 2023 at 17:34:47. See the history of this page for a list of all contributions to it.