# nLab connected relation

## In higher category theory

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

$\forall \left(x,y:A\right),\phantom{\rule{thickmathspace}{0ex}}x\nsim y\phantom{\rule{thickmathspace}{0ex}}\wedge \phantom{\rule{thickmathspace}{0ex}}y\nsim x\phantom{\rule{thickmathspace}{0ex}}⇒\phantom{\rule{thickmathspace}{0ex}}x=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 is usually called tight if it is connected.

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

$\forall \left(x,y:A\right),\phantom{\rule{thickmathspace}{0ex}}x\sim y\phantom{\rule{thickmathspace}{0ex}}\vee \phantom{\rule{thickmathspace}{0ex}}y\sim x\phantom{\rule{thickmathspace}{0ex}}\vee \phantom{\rule{thickmathspace}{0ex}}x=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, $<$ 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 $A$ 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:

$\forall \left(x,y:A\right),\phantom{\rule{thickmathspace}{0ex}}x#y\phantom{\rule{thickmathspace}{0ex}}⇒\phantom{\rule{thickmathspace}{0ex}}x\sim y\phantom{\rule{thickmathspace}{0ex}}\vee \phantom{\rule{thickmathspace}{0ex}}y\sim x.$\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 August 24, 2012 20:05:45 by Urs Schreiber (89.204.138.8)