Ishihara's proof technique in constructive analysis (Q1433041): Difference between revisions
From MaRDI portal
Removed claim: author (P16): Item:Q185794 |
Changed an Item |
||
Property / author | |||
Property / author: Douglas S. Bridges / rank | |||
Normal rank |
Revision as of 18:12, 10 February 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Ishihara's proof technique in constructive analysis |
scientific article |
Statements
Ishihara's proof technique in constructive analysis (English)
0 references
15 June 2004
0 references
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.
0 references
sequential continuity
0 references
complete metric spaces
0 references
constructive analysis
0 references