Homotopy Type Theory Dedekind complete Archimedean ordered field > history (Rev #1)

Defintion

An Archimedean ordered field FF is Dedekind complete if

  • 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 the open interval (a,b)(a,b)

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.