We develop the first steps of a constructive theory of uniformities given by pseudometrics and study its relation to the constructive theory of Bishop topologies. Both these concepts are constructive, function-theoretic alternatives to the notion of a topology of open sets. After motivating the constructive study of uniformities of pseudometrics we present their basic theory and we prove a Stone-Cech theorem for them. We introduce the f-uniform spaces and we prove a Tychonoff embedding theorem for them. We study the uniformity of pseudometrics generated by some Bishop topology and the pseudo-compact Bishop topology generated by some uniformity of pseudometrics. Defining the large uniformity on reals we prove a "large" version of the Tychonoff embedding theorem for f-uniform spaces and we show that the notion of morphism between uniform spaces captures Bishop continuity. We work within BISH*, Bishop's informal system of constructive mathematics BISH extended with inductive definitions with rules of countably many premisses.

Constructive uniformities of pseudometrics and Bishop topologies

Petrakis, Iosif
2019-01-01

Abstract

We develop the first steps of a constructive theory of uniformities given by pseudometrics and study its relation to the constructive theory of Bishop topologies. Both these concepts are constructive, function-theoretic alternatives to the notion of a topology of open sets. After motivating the constructive study of uniformities of pseudometrics we present their basic theory and we prove a Stone-Cech theorem for them. We introduce the f-uniform spaces and we prove a Tychonoff embedding theorem for them. We study the uniformity of pseudometrics generated by some Bishop topology and the pseudo-compact Bishop topology generated by some uniformity of pseudometrics. Defining the large uniformity on reals we prove a "large" version of the Tychonoff embedding theorem for f-uniform spaces and we show that the notion of morphism between uniform spaces captures Bishop continuity. We work within BISH*, Bishop's informal system of constructive mathematics BISH extended with inductive definitions with rules of countably many premisses.
2019
uniform spaces
pseudometrics
Bishop spaces
constructive topology
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/1118993
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? ND
social impact