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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.