A point-free characterisation of Bishop locally compact metric spaces

Tatsuji Kawai

Abstract


We give a characterisation of Bishop locally compact metric spaces in terms of formal topology. We identify inhabited enumerably locally compact regular formal topologies as point-free counterpart of Bishop locally compact metric spaces. Specifically, we show that a formal topology is isomorphic to an inhabited enumerably locally compact regular formal topology if and only if it is isomorphic to the localic completion of a Bishop locally compact metric space. The result is obtained in Bishop constructive mathematics with the Dependent Choice.


Full Text:

C2. [PDF]


DOI: http://dx.doi.org/10.4115/jla.2017.9.c2

Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 License.

Journal of Logic and Analysis ISSN:  1759-9008