Commit 2026-05-10 09:03 e0b7a966

View on Github →

feat: supremum of ≤ c ordinals of cardinal ≤ c has cardinal ≤ c (#37573)

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

added theorem Ordinal.card_iSup_Iio_le

added theorem Ordinal.card_iSup_Iio_le_of_lift

added theorem Ordinal.card_iSup_le

added theorem Ordinal.card_iSup_le_lift

added theorem Ordinal.card_sSup_le

modified theorem Ordinal.lift_card_iSup_le_sum_card