mathlib

63014d26 - feat(order/interval): Order intervals (#14807)

feat(order/interval): Order intervals (#14807) Define `nonempty_interval`, the type of nonempty intervals in an order, namely pairs where the second element is greater than the first, and `interval α` as `with_bot (nonempty_interval α)`.