Pseudo-order

In constructive mathematics, a pseudo-order is a constructive generalisation of a linear order to the continuous case. The usual trichotomy law does not hold in the constructive continuum because of its indecomposability, so this condition is weakened. In constructive mathematics, a pseudo-order is a constructive generalisation of a linear order to the continuous case. The usual trichotomy law does not hold in the constructive continuum because of its indecomposability, so this condition is weakened. A pseudo-order is a binary relation satisfying the following conditions: This first condition is simply antisymmetry. It follows from the first two conditions that a pseudo-order is transitive. The second condition is often called co-transitivity or comparison and is the constructive substitute for trichotomy. In general, given two elements of a pseudo-ordered set, it is not always the case that either one is less than the other or else they are equal, but given any nontrivial interval, any element is either above the lower bound, or below the upper bound. The third condition is often taken as the definition of equality. The natural apartness relation on a pseudo-ordered set is given by