Homotopy Type Theory
Dedekind complete Archimedean ordered field > history (Rev #1)
Defintion
An Archimedean ordered field is Dedekind complete if
-
For all terms , the lower bounded open interval is inhabited.
-
For all terms , the upper bounded open interval is inhabited.
-
For all terms and , if and only if is a subinterval of
-
For all terms and , if and only if is a subinterval of
-
For all terms and , if , then is a subinterval of the union of and
-
For all terms and , the intersection of and is a subinterval of the open interval
See also
References
- Steve Vickers, “Localic Completion Of Generalized Metric Spaces I”, TAC
Revision on April 22, 2022 at 02:07:39 by
Anonymous?.
See the history of this page for a list of all contributions to it.