Locally Constant Constructive Functions and Connectedness of Intervals

TL;DR

The paper proves that locally constant constructive functions on intervals are constant and shows that constructive real intervals are connected but can be decomposed into two disjoint sequentially closed sets.

Contribution

It establishes that locally constant constructive functions are globally constant and characterizes the connectedness properties of constructive real intervals.

Findings

Locally constant constructive functions on intervals are constant.

Constructive real intervals are connected.

Such intervals can be decomposed into two disjoint sequentially closed nonempty sets.

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.