
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]\).
constructive mathematics, Continuous maps, intuitionistic logic, Other constructive mathematics, dependent choice
constructive mathematics, Continuous maps, intuitionistic logic, Other constructive mathematics, dependent choice
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 5 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 10% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |
