Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeApr 28th 2017
   • PermaLink
   Author: Urs
   Format: MarkdownItexadded a proof to _[[Urysohn's lemma]]_

   added a proof to Urysohn’s lemma

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeApr 29th 2017
   • PermaLink
   Author: Urs
   Format: MarkdownItexI have expanded the [proof](https://ncatlab.org/nlab/show/Urysohn%27s+lemma#Proof) to be real careful about the argument for the continuity of the Urysohn function.

   I have expanded the proof to be real careful about the argument for the continuity of the Urysohn function.

3. • CommentRowNumber3.
   • CommentAuthorTodd_Trimble
   • CommentTimeApr 29th 2017
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexNice job, Urs!

   Nice job, Urs!

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeApr 29th 2017
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks, Todd. I just noticed that I still had a gap in the proof of continuity. I have now filled in the missing details [here](https://ncatlab.org/nlab/show/Urysohn's+lemma#PreimagesOfTheSubbaseOpens). In particular this shows that the argument does require excluded middle.

   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.

5. • CommentRowNumber5.
   • CommentAuthorTobyBartels
   • CommentTimeMay 3rd 2017
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexIf 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.)

   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.)

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeMay 3rd 2017
   • (edited May 3rd 2017)
   • PermaLink
   Author: Urs
   Format: MarkdownItexTrue. 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.

   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.

7. • CommentRowNumber7.
   • CommentAuthornLab edit announcer
   • CommentTimeDec 6th 2018
   • PermaLink
   Author: nLab edit announcer
   Format: MarkdownItex$C$ and $U$ were in the opposite position previously in this line near the top of the proof: $$ C \subset V \subset Cl(V) \subset U $$ but $C \subset U$, so that cannot have been correct. J.Martin <a href="https://ncatlab.org/nlab/revision/diff/Urysohn%27s+lemma/12">diff</a>, <a href="https://ncatlab.org/nlab/revision/Urysohn%27s+lemma/12">v12</a>, <a href="https://ncatlab.org/nlab/show/Urysohn%27s+lemma">current</a>

   $C$ and $U$ were in the opposite position previously in this line near the top of the proof:

   $$C \subset V \subset Cl(V) \subset U$$

   but $C \subset U$, so that cannot have been correct.

   J.Martin

   diff, v12, current