Apartness Between Sets

In this–perhaps the most important, and certainly the most technically complex– chapter of the book we extend the notion of point-set (pre-)apartness axiomatically to one of (pre-)apartness between subsets of an inhabited set X. We then study quasi-uniform spaces as an important type of set-set apartness space. In contrast to the counterpart classical theory of proximity spaces, it turns out that the constructive theory of apartness spaces is larger than that of quasi-uniform spaces. In Section 3.3 we explore the connection between strong continuity–the natural set-set extension of the notion of continuity–and uniform continuity. In the next section we introduce and compare various structures that form natural settings for various types of conver- gence in Y X. Section 3.5 introduces totally Cauchy nets in pre-apartness spaces, and develops a number of highly technical results relating totally Cauchy and uniformly Cauchy nets, and corresponding notions of completeness, in a uniform space. The section ends with a uniform-space analogue of Bishop's lemma for locatedness, which leads us neatly into a section covering almost locatedness, a notion that appears to be almost as powerful as the standard one of locatedness for metric spaces. We then construct the product of two apartness spaces, showing how various (but not all) important properties pass between a product space and its factors. This prepares us for a section that deals with proximal connectedness. The penultimate section of the chapter shows how, with a given apartness, we can produce an associated structure that is almost a uniform one (classically, it is a totally bounded uniform structure) and that has a number of interesting properties; in particular, using this structure, we obtain a positive concept of nearness/proximity of sets. The final section deals with Diener's approach to compactness in apartness spaces, using his notions of

neat locatedness and neat compactness

.