Commit 2022-03-08 15:58 1597e9a2

View on Github →

feat(set_theory/ordinal_arithmetic): prove enum_ord_le_of_subset (#12199) I also used this as an excuse to remove a trivial theorem and some awkward dot notation.

Estimated changes

Modified src/set_theory/ordinal_arithmetic.lean

deleted def ordinal.enum_ord.order_iso

deleted theorem ordinal.enum_ord.surjective

added theorem ordinal.enum_ord_le_of_subset

added def ordinal.enum_ord_order_iso

added theorem ordinal.enum_ord_surjective

deleted theorem ordinal.enum_ord_zero_le