#
Homotopy Type Theory
Archimedean ordered field > history (Rev #7, changes)

Showing changes from revision #6 to #7:
Added | ~~Removed~~ | ~~Chan~~ged

## Definition

Let $R$ be an ordered field, and let $inj: \mathbb{Z}_{+} \to R$ be the injection of the positive integers $\mathbb{Z}_{+}$ into $R$.

### With strict order

$R$ is an **Archimedean ordered field** if there is a family of dependent terms

$a:R, b:R \vdash \alpha(a, b): ((0 \lt a) \times (0 \lt b)) \to \Vert \sum_{n:\mathbb{Z}_{+}} a \lt inj(n) \cdot b \Vert$

### With positivity

$R$ is an **Archimedean ordered field** if there is a family of dependent terms

$a:R, b:R \vdash \alpha(a, b): (\mathrm{isPositive}(a) \times \mathrm{isPositive}(b)) \to \Vert \sum_{n:\mathbb{Z}_{+}} a \lt inj(n) \cdot b \Vert$

## Examples

## See also

Revision on June 10, 2022 at 11:29:37 by
Anonymous?.
See the history of this page for a list of all contributions to it.