Successor and predecessor limits #
We define the predicate
Order.IsSuccLimit for "successor limits", values that don't cover any
others. They are so named since they can't be the successors of anything smaller. We define
Order.IsPredLimit analogously, and prove basic results.
The plan is to eventually replace
Cardinal.IsLimit with the common
Successor limits #
A value can be built by building it on successors and successor limits.
- One or more equations did not get rendered due to their size.
Predecessor limits #
A value can be built by building it on predecessors and predecessor limits.