Metric complements of overt closed sets

TL;DR

This paper demonstrates that points of overt closed subspaces in metric completions of Bishop-locally compact spaces are located, and such subspaces are Bishop compact if also compact, advancing constructive metric space theory.

Contribution

It establishes the locatedness of points in overt closed subspaces and their Bishop compactness under compactness, providing new insights in constructive metric space analysis.

Findings

Points of overt closed subspaces are located.

Compact overt closed subspaces are Bishop compact.

Advances constructive understanding of metric space properties.

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.