Ishihara's proof technique in constructive analysis
type: Item
instance of: scholarly article
title: Ishihara's proof technique in constructive analysis
zbMATH Open document ID: 1075.03034
DOI: 10.1016/S0019-3577(03)90001-2
author: Dirk van Dalen
author: Hajime Ishihara
author: Douglas Bridges
published in: Indagationes Mathematicae. New Series
publication date: 2004-06-15T00:00:00Z
review text: 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.
reviewed by: Peter Schuster
Mathematics Subject Classification ID: 03F60
Mathematics Subject Classification ID: 54E50
zbMATH DE Number: 2075406
zbMATH Keywords: sequential continuity
zbMATH Keywords: complete metric spaces
zbMATH Keywords: constructive analysis
MaRDI profile type: Publication
cites work: Q3679172
cites work: Q5591514
cites work: Q3803111
cites work: Q3754620
cites work: Constructive closed range and open mapping theorems
cites work: Continuity and nondiscontinuity in constructive mathematics
cites work: Continuity properties in constructive mathematics
cites work: Q4838046
cites work: Constructivism in mathematics. An introduction. Volume II
full work available at URL: s0019-3577(03)90001-2
OpenAlex ID: W2064351239
Recommended article: Continuity and nondiscontinuity in constructive mathematics
Recommended article: A proof–technique in uniform space theory
Recommended article: Strong continuity implies uniform sequential continuity
Recommended article: Factoring Out Intuitionistic Theorems: Continuity Principles and the Uniform Continuity Theorem
Recommended article: Sequentially continuous linear mappings in constructive analysis
Recommended article: A continuity principle equivalent to the monotone \(\Pi^0_1\) fan theorem
Recommended article: On proximal convergence in uniform spaces
Recommended article: Q4552740
Recommended article: Bishop's Lemma
Recommended article: Weak continuity properties in constructive analysis
description: scientific article; zbMATH DE number 2075406