and were in the opposite position previously in this line near the top of the proof:
but , so that cannot have been correct.
J.Martin
]]>True. There are so many uses of excluded middle in the standard arguments. I meant the one that stands out explicitly when one says “let’s assume the opposite”, but of course, as you highlight, before one gets there one has already used it all over the place.
]]>If you're not going to use excluded middle, then you probably want to talk about open subspaces anyway. Then a space is normal iff, whenever , there exist and such that , , and (with everything here being an open subspace). This fixes a nonconstructive argument that was already at the very beginning of the proof: the claim that is open. In fact, it gets us as far as the entire sequence of and for dyadic rational (using dependent choice to complete the sequence). But defining by infima is already problematic, since an infimum might not be located, hence might not (even when bounded) be a real number in the usual sense. The proof breaks down here, even before you prove continuity. (There might be a theorem about locales instead, but that would look sufficiently different that it should be considered separately.)
]]>Thanks, Todd.
I just noticed that I still had a gap in the proof of continuity. I have now filled in the missing details here.
In particular this shows that the argument does require excluded middle.
]]>Nice job, Urs!
]]>I have expanded the proof to be real careful about the argument for the continuity of the Urysohn function.
]]>added a proof to Urysohn’s lemma
]]>