论文标题
局部恒定的建设性函数和间隔的连接性
Locally Constant Constructive Functions and Connectedness of Intervals
论文作者
论文摘要
我们证明，在间隔上，每个局部恒定的构建函数实际上都是恒定的函数。这回答了安德烈·鲍尔（Andrej Bauer）提出的一个问题。作为一个相关的结果，我们表明，实际上是连接了由建设性实数组成的间隔，但可以分解为两个顺序闭合的非巨型集合的不相交联合。
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.
