arXiv · 2006.00020
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.
Explore related subjects
Keep this discovery
Viktor Chernov. 2020-05-29. Locally Constant Constructive Functions and Connectedness of Intervals. https://doi.org/10.1093/logcom/exaa038
Cite the original work for its findings. Save a collection to share your selection of sources.