Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Adding reference
as a construction of the locale of real numbers can be found in section 5.3 of that article
Anonymous
added reference:
Anonymous
In section 5, it is stated that the join of two opens, defined as shown using the zig-zag lemma is also open.
Let , and let be the union of the and let be the union of the as subsets of the the set of real numbers. It is clear that these are all open subsets of the set and therefore that their associated relations are opens in the locale . It seems that the join of and “contains” whenever , but is not “contained in” the join. Does this not contradict the 4th property opens in the locale of real numbers are required to satisfy?
— Casey (guest)
In the section “Using the Dedekind real numbers”, it mentions defining a function on the locale, from a function on the set of Dedkind reals. Looks a bit too much like the derivative, to me.
@David # 8:
That was done by the anonymous contributor from the edits announced at the top of the page. I certainly don't object to changing it. (In the long run, I'd like the page to have an elementary description of the continuous maps like it has for the opens etc.)
(This is what I needed the stronger version of the Zigzag Lemma for, by the way.)
My friend (and landlord here in Edinburgh) Michael Fourman has read this page with interest and may have some comments. He is carefully studying the work of Brouwer, and trying to rework some of it using topos theory.
1 to 16 of 16