## 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)$ ## See also ## * [[Archimedean ordered integral domain]] * [[interval-complete Archimedean ordered integral domain]] * [[Dedekind real numbers]]