Documentation

Construct an interval from a pair of points.

If a <~ b then a ... b = Empty.

Obtain the endpoints of an interval.

Construct an interval containing a single point.

>>> singleton 1
1 ... 1

\( X_\geq(x) = \{ y \in X | y \geq x \} \)

Construct the upper set of an element x.

This function is monotone wrt the containment order.

\( X_\leq(x) = \{ y \in X | y \leq x \} \)

Construct the lower set of an element x.

This function is antitone wrt the containment order.

The empty interval.

>>> empty
Empty