Metric Double Complements of Convex Sets

In constructive mathematics the metric complement of a subset S of a metric space X is the set -S of points in X that are bounded away from S. In this note we discuss, within Bishop’s constructive mathematics, the connection between the metric double complement, -(-K), and the logical double complement, not not K, where K is a convex subset of a normed linear space X. In particular, we prove that if K has inhabited interior, then -(-K) equals the interior of not not K, that the hypothesis of inhabited interior can be dropped in the finite-dimensional case, and that we cannot constructively replace the interior of not not K by that of K in these results.