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

Showing changes from revision #8 to #9:
Added | ~~Removed~~ | ~~Chan~~ged

## Definition

< Archimedean field

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

~~
~~~~
~~
Last revised on June 16, 2022 at 14:40:55.
See the history of this page for a list of all contributions to it.