Theorem ordinal.sup_eq_lsub
Modification history
2022-05-27 23:26
src/set_theory/ordinal/arithmetic.lean
refactor(set_theory/ordinal/*): `ordinal.succ` → `order.succ` (#14243) …
Modified ordinal.sup_eq_lsubView on Github →2022-03-14 05:19
src/set_theory/ordinal_arithmetic.lean
refactor(set_theory/ordinal_arithmetic): Turn various results into simp lemmas (#12661) …
Added ordinal.sup_eq_lsubView on Github →