[FOM] continuing problems with constructive continuity?
b.spitters at cs.ru.nl
Tue Feb 12 16:15:55 EST 2008
As you know these issues are close to my heart.
The crucial observation is that in order to prove that a continuous morphism
representing a uniformly continuous function f from [0,1] to (0,1] in fact
maps into the formal open subspace (0,1] of [0,1]. This requires (some form
of) the fan theorem. Knowing that f(x)>0 for all x in [0,1] is not enough.
Similarly, the fan theorem is needed to prove that inf f >0.
I hope that this is enough to reconstruct the answers to the rest of your
I am working on a paper where these and related issues are explained at
length, but this will take some time.
More information about the FOM