Separatedness in constructive topology (Q1419690)

This interesting paper continues the authors' extensive study of the constructive aspects of topological spaces. Classically, Hausdorff topological spaces may be characterized by any one of three (classically equivalent) conditions. These conditions (stated quite imprecisely here) are: (H) Distinct points have disjoint open neighborhoods. (N1) A net may have at most one limit. (N2) If a net converges to a point, then it is eventually bounded away from any other point. The paper determines the constructive relationships between these conditions. The various terms, such as distinct, disjoint, and complement, are given precise definitions, which include several constructively-distinct variations. The main results are that (H) and (N2) are constructively equivalent, and if the inequality relation has a certain extra property, they imply (N1). Brouwerian examples are given to show that these results are the best possible in a constructive framework.