Order sum (source code)

= Order sum
{title2=$A+B$}

The order sum $A+B$ is the disjoint union of two <total orders>, preserving each order and placing every element of $A$ before every element of $B$. For example $\mathbb N+\mathbb Z$ has a least element but also has elements with infinitely many predecessors.