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

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

Defintion

< real number

An

Archimedean ordered integral domain FF is Dedekind complete if

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

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

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

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

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

  • For all terms a:Fa:F and b:Fb:F, if a<ba \lt b, then FF is a subinterval of the union of (a,)(a, \infty) and (,b)(-\infty, b)

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

See also

Revision on June 10, 2022 at 15:38:56 by Anonymous?. See the history of this page for a list of all contributions to it.