mathlib3

767aeb39 - feat(order/succ_pred/limit): Successor and predecessor limits (#15001)

feat(order/succ_pred/limit): Successor and predecessor limits (#15001) We define a successor limit as a value that isn't a successor of anything but perhaps itself, and likewise for predecessors. The plan is to use this to redefine limit ordinals and limit cardinals.