Homotopy Type Theory Archimedean ordered integral domain > history (Rev #1)

Definition

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

Examples

See also

Revision on March 11, 2022 at 22:51:54 by Anonymous?. See the history of this page for a list of all contributions to it.