Commit 2024-11-01 19:53 568d74e5

View on Github →

feat(SetTheory/Cardinal/Arithmetic): cardinality of supremum is at most sum of cardinalities (#17845)

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Arithmetic.lean

added theorem Ordinal.card_iSup_Iio_le_card_mul_iSup

added theorem Ordinal.card_iSup_Iio_le_sum_card

added theorem Ordinal.card_iSup_le_sum_card

added theorem Ordinal.lift_card_iSup_le_sum_card