Theorem ordinal.is_normal.lt_nfp
Modification history
2022-02-03 12:53
src/set_theory/ordinal_arithmetic.lean
feat(set_theory/principal): Principal ordinals are unbounded (#11755) …
Deleted ordinal.is_normal.lt_nfpView on Github →2022-01-31 20:42
src/set_theory/ordinal_arithmetic.lean
feat(set_theory/ordinal_arithmetic, set_theory/cardinal_ordinal): `deriv` and `aleph` are enumerators (#10987) …
Modified ordinal.is_normal.lt_nfpView on Github →