cardinal_ordinal): `deriv` and `aleph` are enumerators (#10987)

Commit

3 years ago

feat(set_theory/ordinal_arithmetic, set_theory/cardinal_ordinal): `deriv` and `aleph` are enumerators (#10987) We prove `deriv_eq_enum_fp`, `ord_aleph'_eq_enum_card`, and `ord_aleph_eq_enum_card`.

Author

vihdzp

Parents

750f53c8

mathlib3 719b7b06 - feat(set_theory/ordinal_arithmetic, set_theory/cardinal_ordinal): `deriv` and `aleph` are enumerators (#10987)

mathlib3
719b7b06 - feat(set_theory/ordinal_arithmetic, set_theory/cardinal_ordinal): `deriv` and `aleph` are enumerators (#10987)