On local non‐compactness in recursive mathematics
Jakob Grue Simonsen · Mathematical logic quarterly · 2006
Abstract A metric space is said to be locally non‐compact if every neighborhood contains a sequence that is eventually bounded away from every element of the space, hence contains no accumulation point. We show within recursive mathematics that a nonvoid complete metric space is locally non‐compact iff it is without isolated points. The result has an interesting consequence in computable analysis: If a complete metric space has a computable witness that it is without isolated points, then every neighborhood contains a computable sequence that is eventually computably bounded away from every computable element of the space. (© 2006 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)