Locally constant constructive functions and connectedness of intervals
Viktor Petrovich Chernov · Journal of Logic and Computation · 2020
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 [ 1]. 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 nonempty sets.