Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-31 20:42 719b7b06

View on Github →

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.

Estimated changes

Modified src/set_theory/cardinal_ordinal.lean

added theorem cardinal.eq_aleph'_of_eq_card_ord

added theorem cardinal.eq_aleph_of_eq_card_ord

added theorem cardinal.ord_aleph'_eq_enum_card

added theorem cardinal.ord_aleph_eq_enum_card

added theorem cardinal.ord_card_unbounded'

added theorem cardinal.ord_card_unbounded

Modified src/set_theory/ordinal_arithmetic.lean

added theorem ordinal.deriv_eq_enum_fp

modified theorem ordinal.deriv_limit

added theorem ordinal.is_normal.fp_iff_deriv'

modified theorem ordinal.is_normal.fp_iff_deriv

modified theorem ordinal.is_normal.le_nfp

modified theorem ordinal.is_normal.lt_nfp

added theorem ordinal.is_normal.nfp_unbounded