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.
This theorem, with a constructive proof, is now at convergence space. (The usual proof in undergraduate metric-space theory uses both excluded middle and countable choice1, so I wrote this mostly to verify that it is actually perfectly constructive in the general setting.)
ETA: And the straightforward generalization to nonsequential spaces would use choice of arbitrarily high cardinality. ↩
Where? Ah, here.
Yes, I forgot that I could link directly to it.
The proof is pretty sketchy, especially considering that the theorem as stated actually has 4 parts. But I do think that all of the steps are pretty obvious nose-following except for the bit that I wrote down. (Even that is arguably nose-following; I mean, what could you possibly look at besides the neighbourhood filter? But I was worried for a little while that it might not actually be constructive, so it's helpful to me to have it.)
One might also write out how they're all reflective subcategories. That's probably also pretty obvious, but I haven't thought the whole thing through.
1 to 5 of 5