A Constructive Uniform Continuity Theorem (Q3148703)

The celebrated uniform continuity theorem of classical mathematics states that a pointwise continuous function with metric domain is uniformly continuous if that domain is compact (which, for the purposes of constructive mathematics, is taken to mean totally bounded and complete). While the theorem remains valid within the framework of intuitionistic mathematics strengthened by the principle of continuous choice, it is known to fail in weaker constructive systems (e.g., Markov-style recursive mathematics). In hopes of redressing this difficulty, the authors of the present paper prove, within the confines of intuitionistic logic enriched with the principle of dependent choice, the following constructive uniform continuity theorem: A strongly continuous function with metric domain is uniformlv continuous if that domain is totally bounded (not necessarily complete). [What strong continuity means in the present context is explained as follows. Given a metric space \((X,d)\), define two subsets \(A\) and \(B\) of \(X\) to be apart if there is some positive real number \(r\) such that \(d(a,b)\geq r\) for all \(a\in A\) and \(b\in B\). A function \(f:X\to Y\) between metric spaces is then strongly continuous if \(A\) and \(B\) are apart in \(X\) whenever the images \(f[A]\) and \(f[B]\) are apart in \(Y]\).