Locally Non-compact Spaces and Continuity Rinciples
Alexander Simpson, Andrej Bauer · 2003
We give a constructive proof that Baire space embeds in any inhabited locally non-compact complete separable metric space, X, in such a way that every sequentially continuous function from Baire space to Z extends to a function from X to R. As an application, we show that, in the presence of certain choice and continuity principles, the statement “all functions from X to R is continuous” is false. This generalizes a result previously obtained by Escardo and Streicher, in the context of “domain realizability”, for the special case X = C[0, 1].