Homotopy Type Theory
Dedekind complete Archimedean ordered integral domain > history (Rev #3)
Defintion
An Archimedean ordered integral domain is Dedekind complete if
-
For all terms and , the open interval is inhabited.
-
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
See also
Revision on May 12, 2022 at 00:44:20 by
Anonymous?.
See the history of this page for a list of all contributions to it.