[FOM] continuing problems with constructive continuity?

[b.spitters@cs.ru.nl]

Dear Frank,

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

I am working on a paper where these and related issues are explained at 
length, but this will take some time.

Best,

Bas