A note on nondiscontinuity in constructive mathematics
Satoru Yoshida · 2002
In constructive recursive mathematics of Markov’s school, every mapping of a complete metric space into a metric space is sequentially continuous [1, Theorem 3.2.2], and Ishihara also showed it in [2, Theorem 1] by proving that it is equivalent to ¬WLPO within Bishop-style constructive mathematics. In this paper, we show that Lemma 3.2.1, Theorems 3.2.2 and 3.3.3 of [1] and ¬WLPO are equivalent in Bishop’s framework. Consequently, this paper gives another proof of [2, Theorem 1]. The following is WLPO: For any binary sequence {αn}, either there is no n such that αn = 1 or there is not no n such that αn = 1. Note that ¬ WLPO is true in constructive recursive mathematics and Brouwer’s intuitionistic mathematics respectively; see [1, Corolary 3.1.5 and Proposition 5.2.1] for more details. An operation from a set X to a set Y is a mapping of X into the set of all inhabited subsets of Y. A mapping f of a metric space X into a metric space Y is sequentially nondiscontinuous if for a sequence {xn} in X converging to x in X and a real number δ, what d ′ (f(xn), f(x)) ≥ δ for all n implies δ ≤ 0.