Homotopy Type Theory Dedekind complete Archimedean ordered integral domain > history (Rev #4, changes)

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

Defintion

An

Archimedean ordered integral domain $F$ is Dedekind complete if

• For all terms $a:F$ and $b:F$, the open interval $(a,b)$ is inhabited.

• For all terms $a:F$, the lower bounded open interval $(a,\infty)$ is inhabited.

• For all terms $a:F$, the upper bounded open interval $(-\infty,a)$ is inhabited.

• For all terms $a:F$ and $b:F$, $a \lt b$ if and only if $(b,\infty)$ is a subinterval of $(a,\infty)$

• For all terms $a:F$ and $b:F$, $b \lt a$ if and only if $(-\infty,b)$ is a subinterval of $(-\infty,a)$

• For all terms $a:F$ and $b:F$, if $a \lt b$, then $F$ is a subinterval of the union of $(a, \infty)$ and $(-\infty, b)$

• For all terms $a:F$ and $b:F$, the intersection of $(a,\infty)$ and $(-\infty,b)$ is a subinterval of $(a,b)$