Formally continuous functions on Baire space
Logic
2017-10-25 v1 Logic in Computer Science
Abstract
A function from Baire space to the natural numbers is called formally continuous if it is induced by a morphism between the corresponding formal spaces. We compare formal continuity to two other notions of continuity on Baire space working in Bishop constructive mathematics: one is a function induced by a Brouwer-operation (i.e. inductively defined neighbourhood function); the other is a function uniformly continuous near every compact image. We show that formal continuity is equivalent to the former while it is strictly stronger than the latter.
Cite
@article{arxiv.1710.08755,
title = {Formally continuous functions on Baire space},
author = {Tatsuji Kawai},
journal= {arXiv preprint arXiv:1710.08755},
year = {2017}
}
Comments
13 pages