# Start a new discussion

## Not signed in

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

## Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeApr 28th 2017

added a proof to Urysohn’s lemma

• CommentRowNumber2.
• CommentAuthorUrs
• CommentTimeApr 29th 2017

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

• CommentRowNumber3.
• CommentAuthorTodd_Trimble
• CommentTimeApr 29th 2017

Nice job, Urs!

• CommentRowNumber4.
• CommentAuthorUrs
• CommentTimeApr 29th 2017

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.

• CommentRowNumber5.
• CommentAuthorTobyBartels
• CommentTimeMay 3rd 2017

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

• CommentRowNumber6.
• CommentAuthorUrs
• CommentTimeMay 3rd 2017
• (edited May 3rd 2017)

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