Documentation

$\forall a, b: ((a \# b) \vee (b \# a))$

For example, ≥ is a connex relation, while 'divides evenly' is not.

A connex relation cannot be symmetric, except for the universal relation.

$\forall a, b: \neg (a \equiv b) \Rightarrow ((a \# b) \vee (b \# a))$

A binary relation is semiconnex if it relates all pairs of _distinct_ elements in some way.

A relation is connex if and only if it is semiconnex and reflexive.

$\forall a, b: \neg (a \doteq b) \Rightarrow ((a \# b) \vee (b \# a))$

$\forall a, b, c: ((a \# b) \vee (a \equiv b) \vee (b \# a)) \wedge \neg ((a \# b) \wedge (a \equiv b) \wedge (b \# a))$

Note that trichotomous (>) should hold for any Ord instance.

$\forall a, b, c: ((a \# b) \vee (a \doteq b) \vee (b \# a)) \wedge \neg ((a \# b) \wedge (a \doteq b) \wedge (b \# a))$

In other words, exactly one of $a \# b$, $a \doteq b$, or $b \# a$ holds.

For example, > is a trichotomous relation, while ≥ is not.