Commit 2021-12-18 18:09 fec084c3
View on Github →feat(order/cover): The covering relation (#10676)
This defines a ⋖ b
to mean that a < b
and there is no element in between. It is generally useful, but in particular in the context of polytopes and successor orders.