Showing changes from revision #2 to #3:
Added | Removed | Changed
Since a dense strict order has an order topology associated with it, one could create the locale with the open sets of a dense strict order, which are the open intervals in the dense strict order.
er, better
Let be a type with a dense strict order . Let and be bounded open intervals in , be a lower bounded open interval in , and be an upper bounded open interval in . is the unbounded open interval in , and is denoted as . Then if and , if , and if .
By defintion, every bounded open interval , every lower bounded open interval , every upper bounded open interval , and , which means that is the top element in the large poset of open intervals in .
The intersection of two open intervals and is simply of the two subtypes.
The empty interval is any interval where , and by definition it is the bottom element in the large poset of open intervals in .
The union of two open intervals and , , exists and is equal to if and only if .
In fact, for any family of open intervals for , for if and only if the union of the family of open intervals exist and is equal to
The union of an arbitrary family of open intervals is defined such that for every open interval
if and only if (1) is the empty interval or (2) there exists a family of open intervals for such that
and
to be continued…
I’m probably going to use Steve Vicker’s presentation rather than Toby Bartel’s.
Last revised on June 10, 2022 at 15:49:58. See the history of this page for a list of all contributions to it.