Ishihara's proof technique in constructive analysis (Q1433041)

Two related lemmas of \textit{H. Ishihara} [J. Symb. Log. 56, 1349--1354 (1991; Zbl 0745.03048)] are illuminated, which can be proved -- and proved to be useful -- in sequence-style constructive analysis à la Bishop with countable choice. The second lemma, for instance, assures that if \(f\) is a strongly extensional mapping from a complete metric space \(X\) to an arbitrary metric space, and \((x_n)\) a convergent sequence in \(X\) with limit \(x\), then for each \(\varepsilon >0\) either \(f(x_n)\) is within \(\varepsilon\) of \(f(x)\) for all but finitely many \(n\) or \(f(x_n)\) is distant from \(f(x)\) for infinitely many \(n\). As Bishop's limited principle of omniscience (LPO) follows from the latter alternative, the former holds, and \(f\) is sequentially continuous, wherever this principle fails. Apart from the usefulness of either lemma for doing proofs, more light is thus shed on the well-known phenomenon that all mappings of the aforementioned sort are continuous both in Brouwer's intuitionistic mathematics and in Markov's recursive mathematics, where LPO is contradictory.