Aligning the weak König lemma, the uniform continuity theorem, and Brouwer's fan theorem (Q424539): Difference between revisions

Let WKL be weak König's lemma, UC be the uniform continuity theorem, i.e., the statement that each continuous function \(f:[0,1]^\mathbb{N}\to \mathbb{N}\) is uniformly continuous, and FAN be Brouwer's fan theorem. Classically WKL, UC and FAN are equivalent. FAN is the contraposition of WKL and is the intuitionistic counterpart of WKL. In this paper, these principles are now considered in Bishop-style constructive mathematics (BISH) and it is show that BISH proves \(\mathrm{WKL}\to \mathrm{UC} \to \mathrm{FAN}\).