Closed subsets in Bishop topological groups

Abstract

We introduce the notion of a Bishop topological group i.e., a group X equipped with a Bishop topology of functions F such that the group operations of X are Bishop morphisms with respect to F. A closed subset in the neighborhood structure of X induced by its Bishop topology F is defined in a positive way i.e., not as the complement of an open subset in X. The corresponding closure operator, although it is not topological, in the classical sense, does not involve sequences. As countable choice (CC) is avoided, and in agreement with Richman's critique on the use of CC in constructive mathematics, the fundamental facts on closed subsets in Bishop topological groups shown here have a clear algorithmic content. We work within Bishop's informal system of constructive mathematics BISH, without countable choice, equipped with inductive definitions with rules of countably many premises.