Commit 2021-09-18 13:22 10a62016

View on Github →

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.

Estimated changes

Modified src/order/conditionally_complete_lattice.lean

added theorem not_mem_of_cSup_lt

added theorem not_mem_of_lt_cInf

Modified src/set_theory/ordinal.lean

added theorem ordinal.Inf_eq_omin

added theorem ordinal.Inf_mem

added theorem ordinal.bot_eq_zero

added theorem ordinal.induction