Homotopy Type Theory Archimedean ordered integral domain > history (changes)

Showing changes from revision #7 to #8: Added | Removed | Changed

Definition

< Archimedean integral domain

Let

RR be an ordered integral domain, and let inj: +Rinj: \mathbb{Z}_{+} \to R be the injection of the positive integers +\mathbb{Z}_{+} into RR.

With strict order

RR is an Archimedean ordered integral domain if there is a family of dependent terms

a:R,b:Rα(a,b):((0<a)×(0<b)) n: +a<inj(n)ba: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

RR is an Archimedean ordered integral domain if there is a family of dependent terms

a:R,b:Rα(a,b):(isPositive(a)×isPositive(b)) n: +a<inj(n)ba: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 19:58:09. See the history of this page for a list of all contributions to it.