Abstract: Locatedness is one of the fundamental notions in constructive mathematics. The existence of a positivity predicate on a locale, i.e. the locale being overt, or open, has proved to be fundamental in constructive locale theory. We show that the two notions are intimately connected. Bishop defines a metric space to be compact if it is complete and totally bounded. A subset of a totally bounded set is again totally bounded iff it is located. So a closed subset of a Bishop compact set is Bishop compact iff it is located. We translate this result to formal topology. `Bishop compact' is translated as compact and overt. We propose a definition of located predicate on subspaces in formal topology. We call a sublocale located if it can be presented by a formal topology with a located predicate. We prove that a closed sublocale of a compact regular locale has a located predicate iff it is overt. Moreover, a Bishop-closed subset of a complete metric space is Bishop compact -- that is, totally bounded and complete -- iff its localic completion is compact overt. Finally, we show by elementary methods that the points of the Vietoris locale of a compact regular locale are precisely its compact overt sublocales. We work constructively, predicatively and avoid the use of the axiom of countable choice. Consequently, all our results are valid in any predicative topos.
Recommendations
Cites work
- scientific article; zbMATH DE number 3853067 (Why is no real title available?)
- scientific article; zbMATH DE number 3853324 (Why is no real title available?)
- scientific article; zbMATH DE number 4152376 (Why is no real title available?)
- scientific article; zbMATH DE number 4002093 (Why is no real title available?)
- scientific article; zbMATH DE number 4070894 (Why is no real title available?)
- scientific article; zbMATH DE number 3664922 (Why is no real title available?)
- scientific article; zbMATH DE number 3759128 (Why is no real title available?)
- scientific article; zbMATH DE number 3780545 (Why is no real title available?)
- scientific article; zbMATH DE number 3787631 (Why is no real title available?)
- scientific article; zbMATH DE number 2019830 (Why is no real title available?)
- scientific article; zbMATH DE number 1367720 (Why is no real title available?)
- scientific article; zbMATH DE number 2117177 (Why is no real title available?)
- scientific article; zbMATH DE number 1420837 (Why is no real title available?)
- scientific article; zbMATH DE number 3428899 (Why is no real title available?)
- scientific article; zbMATH DE number 3216177 (Why is no real title available?)
- scientific article; zbMATH DE number 2222240 (Why is no real title available?)
- scientific article; zbMATH DE number 2247257 (Why is no real title available?)
- scientific article; zbMATH DE number 2247258 (Why is no real title available?)
- A constructive and functorial embedding of locally compact metric spaces into locales
- A constructive proof of the Heine-Borel covering theorem for formal reals
- About Stone's notion of spectrum
- Adjoints and the image of the ball
- Almost locatedness in uniform spaces
- An extension of the Galois theory of Grothendieck
- Apartness, compactness and nearness
- Aspects of general topology in constructive set theory
- Compactification of Frames
- Compactness in locales and in formal topology
- Constructive points of powerlocales
- Constructivism in mathematics. An introduction. Volume II
- Continuous domains as formal spaces
- Exact approximations to Stone-Čech compactification
- Formal systems for some branches of intuitionistic analysis
- Formal topology and constructive mathematics: the Gelfand and Stone-Yosida representation theorems
- Generalized real numbers in constructive mathematics
- Geometric Intuition and Elementary Constructive Analysis
- Inductively generated formal topologies.
- Integrals and valuations
- Intuitionism. An introduction
- Localic completion of generalized metric spaces. II: Powerlocales
- Located Operators
- Locating subsets of a Hilbert space
- Locating subsets of a normed space
- Metric complements of overt closed sets
- On the \(T_{1}\) axiom and other separation properties in constructive point-free and point-set topology
- On the collection of points of a formal space
- Open sublocales of localic completions
- Open subspaces of locally compact metric spaces
- Proper maps of locales
- Remarks on the Stone-Čech and Alexandroff compactifications of locales
- Sheaves in geometry and logic: a first introduction to topos theory
- Some points in formal topology.
- Sublocales in formal topology
- The ``closed subgroup theorem for localic herds and pregroupoids
- Weak compactness in constructive spaces
Cited in
(9)- scientific article; zbMATH DE number 5178676 (Why is no real title available?)
- Sublocales in formal topology
- Metric complements of overt closed sets
- Almost locatedness in uniform spaces
- Apartness, sharp elements, and the Scott topology of domains
- Structural, point-free, non-Hausdorff topological realization of Borel groupoid actions
- A point-free characterisation of Bishop locally compact metric spaces
- Converses of Bishop's lemma on located sets
- Sharp elements and apartness in domains
This page was built for publication: Locatedness and overt sublocales
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q638474)
