Effective properties of sets and functions in metric spaces with computability structure

AbstractWe consider an abstract metric space with a computability structure and an effective separating set. In this article, we also introduce an effectively σ-compact space. The computability of real-valued functions on such a space is defined. It is shown that some of typical propositions in a metric space, namely Baire category theorem, Tietze's extension theorem and decomposition of unity, can be effectivized. It is also proved that computable functions are dense in continuous functions