Metric complements of overt closed sets |
| |
| Authors: | Thierry Coquand Erik Palmgren Bas Spitters |
| |
| Institution: | 1. Computer Science and Engineering, Chalmers University of Technology and University of Gothenburg, 412 96 G?teborg, Sweden;2. Swedish Collegium for Advanced Study, Linneanum Thunbergsv?gen 2, 752 38 Uppsala, Sweden;3. Matematiska Institutionen, Uppsala Universitet, P.O. Box 480, 751 06 Uppsala, Sweden;4. Radboud University, Department of Computer Science, P.O. Box 9010, 6500 GL Nijmegen, The Netherlands |
| |
| Abstract: | We show that the set of points of an overt closed subspace of a metric completion of a Bishop‐locally compact metric space is located. Consequently, if the subspace is, moreover, compact, then its collection of points is Bishop‐compact. © 2011 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim |
| |
| Keywords: | Constructive analysis locales formal topology MSC (2010) 06D22 28C05 |
|
|
