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.(c) 2022 Elsevier B.V. All rights reserved.

Closed subsets in Bishop topological groups

Petrakis, Iosif
2022-01-01

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.(c) 2022 Elsevier B.V. All rights reserved.
2022
Constructive topological algebra
Bishop topological groups
Closed sets
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/1118937
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 1
social impact