Locally Constant Constructive Functions and Connectedness of Intervals

Abstract

We prove that every locally constant constructive function on an interval is in fact a constant function. This answers a question formulated by Andrej Bauer. As a related result we show that an interval consisting of constructive real numbers is in fact connected, but can be decomposed into the disjoint union of two sequentially closed nonempy sets.

4 pages, 0 figures. Minor corrections and improvements. References updated

Cited by in corpus (1)

• Types of connectedness of the constructive real number intervals