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.
['Thierry Coquand', 'Erik Palmgren', 'Bas Spitters']
Metric complements of overt closed sets