On a continuity theorem for constructive functions

TL;DR

This paper proves that any everywhere defined constructive map between complete metric spaces that preserves precompactness is locally uniformly continuous, linking classical theorems with constructive analysis.

Contribution

It establishes a continuity theorem for constructive functions, interpreting Brower's fan theorem within Markov's constructive framework.

Findings

Constructive maps preserving precompactness are locally uniformly continuous.

Links classical topological theorems with constructive analysis.

Provides a new interpretation of Brower's fan theorem.

Abstract

One proves that any everywhere defined constructive mapping from a complete metric space into a complete metric space which preserves the property of precompacity of subsets is locally uniformly continuous. This fact can be viewed as interpretation of L. E. J. Brower's fan theorem in terms of A. A. Markov's constructive analysis.