In constructive point-set topology, there are a variety of notions of when a subspace is located. This varies depending on what kind of space one is discussing, and even for a given kind of space, there are sometimes various weaker and stronger notions of locatedness. Typically (if not always), these concepts are trivial in classical mathematics.
A located subspace should be viewed as a nice subspace, ruling out pathological counterexamples that exist for logical rather than topological reasons. For example, given any space and any truth value , there exists a subspace , and these can seem very strange for undecidable ; but typically (if not always), this subspace will only be located if is true or false.
Given a metric space , a subspace of , and a point of , we commonly define the distance from to (or from to ) as an infimum:
In constructive mathematics, this infimum is generally an upper real number, even if (as is usual) we require the distances to always be a located real number.
The subspace is located (or metrically located to be specific) if, for each point , is located. (Although we are defining located subspaces in terms of located real numbers, this is backwards historically; the term was first used, by Jan Brouwer, to refer to subsets.)
We should really speak of extended upper/located real numbers, in case might be empty or we wish to apply the concept in an extended metric space. But at least if is bounded? and inhabited, then a located subspace must be empty or inhabited.
Note that there is a smaller complete lattice than the upper reals that contains the located reals and in which we could take the infimum, namely the MacNeille real numbers. However, the inclusion of MacNeille reals into upper reals does not preserve infima (though it does preserve suprema), and in the definition of located subspace we really do want to assert that the upper real infimum, not the MacNeille real infimum, is a located real. This is because upper real infima, unlike MacNeille real infima, have the property that if then there is an such that , which is crucial for the desired behavior of locatedness.
If is a uniform space, Bridges et. al. define a subspace to be almost located if for any entourage , there is an entourage such that . In other words, every point is either within of some point of or not within of any point of .
Since this seems the most natural notion of locatedness for uniform spaces, one might naturally also call such a subspace uniformly located. However, note that even if is a metric space, metric locatedness is strictly stronger than uniform locatedness; Bridges et. al. give an example showing that metric locatedness is not a uniform invariant (while uniform locatedness is of course).
Given a topological space and a subspace of , is located (or topologically located to be specific) if, given any point and neighbourhood of , either is inhabited or some other neighbourhood of is disjoint with .
See Section 7.3 of Troelstra & van Dalen.
Any singleton subset of a metric space, or more generally any finite subset, is metrically located, since we can take the minimum of any finite set. A singleton subset of a uniform space is uniformly located if and only if the uniform space is regular.
Suppose is a uniformly regular uniform space and that (the underlying set of) is a covert set. Then is uniformly located in .
Since is uniformly regular, for any entourage there is an entourage such that . In particular, for any , for any , we have either or . By covertness of , it follows that either for some , or for all , which is to say that .
Suppose is a uniformly regular uniform space and that is compact in its induced topology. Then is uniformly located in .
Given any entourage , let and be entourages such that (by uniform regularity) and . Let be the interior of . Then , since if then is a neighborhood of contained in (for if then , which is not the case, hence ). Thus, .
Let be the inclusion and the projection. Then . Since is uniformly regular, it is regular. Thus is compact regular, and hence locally compact, so the locale product is spatial. Therefore is both an open map and a proper map of locales. We then have , hence , and so by properness as well. In other words, for every either for all , or there exists a such that . Since , it follows that is almost located.
Douglas Bridges, Hajime Ishihara, Ray Mines, Fred Richman, Peter Schuster, and Luminiţa Vîţă. Almost locatedness in uniform spaces, Czechoslovak Mathematical Journal, Vol. 57 (2007), No. 1, 1–12, web
Anne Sjerp Troelstra & Dirk van Dalen, Constructivism in Mathematics 2.
Various related notions of locatedness are studied in
Last revised on February 12, 2019 at 00:39:43. See the history of this page for a list of all contributions to it.