SEPARATION PROPERTIES IN CONSTRUCTIVE TOPOLOGY
This chapter studies separation properties in topology as done on the basis of the formal system CZF. Until the 1970s, there was only a limited focus on the general notion of a topological space in constructive mathematics, with most attention being paid to metric space notions both in intuitionistic analysis and in Bishop-style constructive analysis. But in later years, because of the development of topos theory, the study of sheaf models, and work on point-free topology, including work on formal topology, the notions of general topology in constructive mathematics have received more attention. This chapter presents a fairly systematic survey of the main separation properties that topological spaces can have in constructive mathematics. These are perhaps the first kinds of properties to consider when moving from the study of metric spaces to the study of general topological spaces.
Oxford Scholarship Online requires a subscription or purchase to access the full text of books within the service. Public users can however freely search the site and view the abstracts and keywords for each book and chapter.
If you think you should have access to this title, please contact your librarian.