Locally Constant Constructive Functions and Connectedness of Intervals
Logic
2020-07-24 v2
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.
Keywords
Cite
@article{arxiv.2006.00020,
title = {Locally Constant Constructive Functions and Connectedness of Intervals},
author = {Viktor Chernov},
journal= {arXiv preprint arXiv:2006.00020},
year = {2020}
}
Comments
4 pages, 0 figures. Minor corrections and improvements. References updated