A uniformly continuous function on [0,1] that is everywhere different from its infimum
William H. Julian, Fred Richman · Pacific Journal of Mathematics · 1984
An example of a uniformly continuous function on [0,1] that is everywhere different from its infimum is constructed in the context of Bishop's constructive mathematics using a consequence of Chruch's thesis.The existence of such a function is shown to be equivalent to the constructive denial of Kδnig's lemma.Conversely Kόnig's lemma is shown to be equivalent to the intuitionistic theorem that every positive uniformly continuous function on [0,1] has a positive infimum.Various applications to constructive mathematics are given.