**analysis** (differential/integral calculus, functional analysis, topology)

metric space, normed vector space

open ball, open subset, neighbourhood

convergence, limit of a sequence

compactness, sequential compactness

continuous metric space valued function on compact metric space is uniformly continuous

…

…

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 $F$ there is a field homomorphism $h:\mathbb{Q}\to F$. $F$ is *Archimedean* if for all elements $a\in F$ and $b\in F$, if $a \lt b$, then there exists a rational number $q\in \mathbb{Q}$ such that $a \lt h(q)$ and $h(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:

Let $F$ be an Archimedean ordered field. A function $f:F \to F$ is **continuous at a point** $c \in F$ if

$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)$

$f$ is **pointwise continuous** in $F$ if it is continuous at all points $c$:

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

The set of all pointwise continuous functions is defined as

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

Let $F$ be an Archimedean ordered field. A function $f:F \to F$ is **differentiable at a point** $c \in F$ if

$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$

$f$ is **pointwise differentiable** in $F$ if it is differentiable at all points $c$:

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

The set of all pointwise differentiable functions is defined as

$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.