# BISH: If a function is pointwise positive, is its infimum positive?

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.

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. The fact that the infimum is greater than zero is then a tautology.

• In response to your edit: yes, the infimum of $f$ now is greater than $0$, but often the new problem becomes to show that $\inf(f)> c$ ... and then we're back at square one. Nov 13 '19 at 13:20
• What my paper shows is that there is no simple way to avoid the Fan Theorem if one wishes continuous functions to have certain nice properties. And I am not convinced that the non-simple ways that have been proposed so far to remediate this are really workable in all areas of mathematics. Nov 13 '19 at 13:23
• To the reader wondering what "BISH" could mean: it seems that it means "the Bishop school of constructive mathematics". Nov 14 '19 at 9:36

(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}]$$