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.