Commit 2024-11-01 19:53 95ecdbc4

View on Github →

feat(SetTheory/Cardinal/Aleph): simpler definition of aleph (#17674) We redefine aleph' o = (omega' o).card and aleph o = (omega o).card.

Estimated changes

deleted theorem Cardinal.alephIdx.init
deleted theorem Cardinal.alephIdx_le
deleted theorem Cardinal.alephIdx_lt
modified theorem Cardinal.aleph_isNormal
added theorem Cardinal.ord_aleph
added theorem Cardinal.ord_preAleph
modified def Cardinal.preAleph
modified theorem Cardinal.preAleph_isNormal
modified theorem Cardinal.succ_aleph0
added theorem Ordinal.card_omega
added theorem Ordinal.card_preOmega
modified theorem Ordinal.aleph_cof
added theorem Ordinal.cof_omega
added theorem Ordinal.cof_preOmega