mathlib

10a62016 - feat(set_theory/ordinal): add conditionally_complete_linear_order_bot instance (#9266)

feat(set_theory/ordinal): add conditionally_complete_linear_order_bot instance (#9266) Currently, it is not possible to talk about `Inf s` when `s` is a set of ordinals. This is fixed by this PR.