### Point-free characterisation of Bishop compact metric spaces

#### Abstract

We give a point-free characterisation of Bishop compact metric spaces in terms of formal topology. We show that the notion of overt compact enumerably completely regular formal topology is a point-free counterpart of that of Bishop compact metric space. Specifically, a formal topology is isomorphic to an overt compact enumerably completely regular formal topology if and only if it is isomorphic to the image of a compact metric space under the localic completion of metric spaces into formal topologies. The result is obtained in Bishop constructive mathematics with the axiom of Dependent Choice.

#### Full Text:

5. [PDF]DOI: https://doi.org/10.4115/jla.2017.9.5

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

Journal of Logic and Analysis ISSN: 1759-9008