< [[nlab:real numbers]] ## Defintion ## An [[Archimedean ordered field]] $F$ is **Dedekind complete** if * For all terms $a:F$, the [[lower bounded open interval]] $(a,\infty)$ is inhabited. $$\alpha:\prod_{a:F} \left[(a, \infty)\right]$$ * For all terms $a:F$, the [[upper bounded open interval]] $(-\infty,a)$ is inhabited. $$\beta:\prod_{a:F} \left[(-\infty, a)\right]$$ * For all terms $a:F$ and $b:F$, $a \lt b$ if and only if $(b,\infty)$ is a subinterval of $(a,\infty)$ $$\gamma:\prod_{a:F} \prod_{b:F} (a \lt b) \cong ((b,\infty) \subseteq (a,\infty)$$ (for all propositions $A$ and $B$, $p:(A \cong B) \cong ((A \to B) \times (B \to A))$) * For all terms $a:F$ and $b:F$, $b \lt a$ if and only if $(-\infty,b)$ is a subinterval of $(-\infty,a)$ $$\delta:\prod_{a:F} \prod_{b:F} (b \lt a) \cong ((-\infty,b) \subseteq (-\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)$ $$\epsilon:\prod_{a:F} \prod_{b:F} (a \lt b) \to (F \subseteq ((a, \infty) \cup (-\infty, b)))$$ * For all terms $a:F$ and $b:F$, the intersection of $(a,\infty)$ and $(-\infty,b)$ is a subinterval of the [[open interval]] $(a,b)$ $$\eta:\prod_{a:F} \prod_{b:F} ((a, \infty) \cap (-\infty, b)) \subseteq (a, b)$$ ## See also ## * [[Archimedean ordered field]] * [[Dedekind real numbers]] * [[locator]] ## References ## * Steve Vickers, “Localic Completion Of Generalized Metric Spaces I”, [TAC](http://www.tac.mta.ca/tac/volumes/14/15/14-15abs.html)