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.
added a proof to Urysohn’s lemma
I have expanded the proof to be real careful about the argument for the continuity of the Urysohn function.
Nice job, Urs!
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.
If you're not going to use excluded middle, then you probably want to talk about open subspaces anyway. Then a space $X$ is normal iff, whenever $G \cup H = X$, there exist $U$ and $V$ such that $G \cup U = X$, $H \cup V = X$, and $U \cap V = \empty$ (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 $U_1$ is open. In fact, it gets us as far as the entire sequence of $C_r$ and $U_r$ for dyadic rational $r$ (using dependent choice to complete the sequence). But defining $f$ 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.)
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.
1 to 7 of 7