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

Showing changes from revision #2 to #3: Added | Removed | Changed

Definition

Let RR be an ordered field, and let inj: +Rinj: \mathbb{Z}_{+} \to R be the injection of the positive integers +\mathbb{Z}_{+} into RR. RR is an Archimedean ordered field 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 31, 2022 at 02:43:27 by Anonymous?. See the history of this page for a list of all contributions to it.