Resolution of the uniform lower bound problem in constructive analysis

摘要

In a previous paper we constructed a full and faithful functor M from the category of locally compact metric spaces to the category of formal topologies (representations of locales). Here we show that for a real-valued continuous function /, M{f) factors through the localic positive reals if, and only if, / has a uniform positive lower bound on each ball in the locally compact space,. We work within the framework of Bishop constructive mathematics, where the latter notion is strictly stronger than point-wise positivity.