Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • 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 XX is normal iff, whenever GH=XG \cup H = X, there exist UU and VV such that GU=XG \cup U = X, HV=XH \cup V = X, and UV=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 1U_1 is open. In fact, it gets us as far as the entire sequence of C rC_r and U rU_r for dyadic rational rr (using dependent choice to complete the sequence). But defining ff 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. CC and UU were in the opposite position previously in this line near the top of the proof:

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

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


    diff, v12, current