On the constructive notion of closure maps
Let A be a subset of the constructive real line. What are the necessary and sufficient conditions for the set A such that A is continuously separated from other reals, i.e., there exists a continuous function f with f?1(0) = A? In this paper, we study the notions of closed sets and closure maps in constructive reverse mathematics.
closure maps constructive reverse mathematics fan theorem.