Formally continuous functions on Baire space

TL;DR

This paper investigates different notions of continuity on Baire space within Bishop constructive mathematics, establishing equivalences and strict inequalities among formal continuity, Brouwer-induced continuity, and uniform continuity near compact images.

Contribution

It demonstrates that formal continuity is equivalent to Brouwer-operation induced continuity and strictly stronger than uniform continuity near compact images.

Findings

Formal continuity equals Brouwer-operation induced continuity.

Formal continuity is strictly stronger than uniform continuity near compact images.

Provides a comparison of continuity notions in constructive mathematics.

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.