Let $f:[0,1] \to \mathbb R$ be a uniformly continuous function such that each value of $f(x)$ is greater than zero. Is its infimum greater than zero in BISH?


I believe that it is indeed the case if one assumes the Fan Theorem. But independent of it, I'm not sure.


[edit]


Note: It's possible to get around this problem in practice by interpreting $f > 0$ to mean that there exists a constant $c$ such that $f(x) > c > 0$ for all $x$. This is an example of a [pseudo-order](https://en.wikipedia.org/wiki/Pseudo-order). The fact that the infimum is greater than zero is then a tautology.



BISH: If a function is pointwise positive, is its infimum positive?
In BISH the follwoing two statements are equivalent:


(i) If $f:[0,1] \to \{y\in\mathbb R\, | \,y>0\}$ is uniformly continuous, then there is $n\in\mathbb N$ such that $\forall x \in [0,1]\ [f(x)>\frac{1}{n}]$


(ii) The Fan Theorem **FT**


This was already proved in Julian, W.H., and Richman, F., 1984, “A uniformly continuous function on [0, 1] that is everywhere different from its infimum”, Pacific Journal of Mathematics,111: 333–340.


A simpler proof, and a lot more consequences, are given in my paper [On the foundations of constructive mathematics --- especially in relation to the theory of continuous functions](https://www.fwaaldijk.nl/foundations%20of%20constructive%20mathematics.pdf)


