Markov's principle, Church's thesis and Lindelöf's theorem (Q1315098)

The paper contains some results in constructive mathematics concerning Markov's Principle (MP) and Extended Church's Thesis (ECT). In particular, the theorem ``Mappings from a complete metric space into a metric space are sequentially continuous'' is proved using a disjunctive form of Church's Thesis only. Moreover, a version of Lindelöf's theorem (``Every open cover of a complete separable metric space has an enumerable subcover'') is proved using ECT only and MP is not needed.