mathlib3
1597e9a2 - feat(set_theory/ordinal_arithmetic): prove `enum_ord_le_of_subset` (#12199)

Commit

3 years ago

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.

Author

vihdzp

Parents

ab6a892b

mathlib3 1597e9a2 - feat(set_theory/ordinal_arithmetic): prove `enum_ord_le_of_subset` (#12199)

mathlib3
1597e9a2 - feat(set_theory/ordinal_arithmetic): prove `enum_ord_le_of_subset` (#12199)