connected relation

A (binary) relation \sim on a set AA is connected if any two elements that are related in neither order are equal:

(x,y:A),xyyxx=y. \forall (x, y: A),\; x \nsim y \;\wedge\; y \nsim x \;\Rightarrow\; x = y .

This is a basic property of linear orders; an apartness relation (or indeed any inequality) is usually called tight if it is connected, in which case equality is its negation.

Using excluded middle, it is equivalent to say that every two elements are related in some order or equal:

(x,y:A),xyyxx=y. \forall (x, y: A),\; x \sim y \;\vee\; y \sim x \;\vee\; x = y .

However, this version is too strong for the intended applications to constructive mathematics. (In particular, <\lt 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 AA is already equipped with a tight apartness #\#. In that case, we say that \sim is strongly connected if any two distinct elements are related in one order or the other:

(x,y:A),x#yxyyx. \forall (x, y: A),\; x \# y \;\Rightarrow\; x \sim y \;\vee\; y \sim x .

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 February 4, 2016 18:49:45 by Toby Bartels (