Types of connectedness of the constructive real number intervals

TL;DR

This paper explores various notions of connectedness in constructive metric spaces, revealing that the constructive real interval's connectedness depends on the specific definitions used, unlike in classical topology.

Contribution

It analyzes different constructive connectedness notions, showing their non-equivalence and impact on the connectedness of the constructive real interval.

Findings

Connectedness depends on the chosen definition in constructive spaces.

The constructive real interval's connectedness varies with different notions.

Classical equivalences do not hold in the constructive setting.

Abstract

We study different notions of connected constructive metric spaces. They differ the types of connected components and how different components relate to each other. These notions are equivalent in classical point set topology but they give differ in the constructive world. In particular the interval of constructive real number appears to be connected if we use some of the definitions of a connected space and it is not connected when we use other definitions. This study is the continuation of the previous work of the author inspired by the question of Andrej Bauer about properties of locally constant functions.