Using excluded middle, it is equivalent to say that every two elements are related in some order or equal:
However, this version is too strong for the intended applications to constructive mathematics. (In particular, on the located Dedekind real numbers satisfies the first definition but not this one.)
On the other hand, there is a stronger notion that may be used in constructive mathematics, if is already equipped with a tight apartness . In that case, we say that is strongly connected if any two distinct elements are related in one order or the other:
Since is connected itself, every strongly connected relation is connected; the converse holds with excluded middle (through which every set has a unique tight apartness).
Revised on August 24, 2012 20:05:45
by Urs Schreiber