Commit 2024-10-16 11:05 fd745ec8

View on Github →

feat(SetTheory/Cardinal/Aleph): define initial ordinals (#16964)

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

added theorem Ordinal.IsInitial.card_le_card

added theorem Ordinal.IsInitial.card_lt_card

added theorem Ordinal.IsInitial.ord_card

added def Ordinal.IsInitial

added def Ordinal.isInitialIso

added theorem Ordinal.isInitial_natCast

added theorem Ordinal.isInitial_omega0

added theorem Ordinal.isInitial_one

added theorem Ordinal.isInitial_ord

added theorem Ordinal.isInitial_zero

added theorem Ordinal.not_bddAbove_isInitial

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

deleted theorem Cardinal.ord_aleph0

Modified Mathlib/SetTheory/Ordinal/Basic.lean

added theorem Cardinal.ord_aleph0