Mathlib Changelog
v4
Changelog
About
Github
Theorem
Ordinal.card_iSup_Iio_le_sum_card
Modification history
2025-03-17 11:54
Mathlib/SetTheory/Cardinal/Arithmetic.lean
refactor(SetTheory/Cardinal/Ordinal): move results (#21857) …
Modified
Ordinal.card_iSup_Iio_le_sum_card
View on Github →
2024-12-12 22:51
Mathlib/SetTheory/Cardinal/Arithmetic.lean
chore(SetTheory/Cardinal/Arithmetic): generalize `card_iSup_Iio_le_sum_card` (#19727) …
Modified
Ordinal.card_iSup_Iio_le_sum_card
View on Github →
2024-11-01 19:53
Mathlib/SetTheory/Cardinal/Arithmetic.lean
feat(SetTheory/Cardinal/Arithmetic): cardinality of supremum is at most sum of cardinalities (#17845)
Added
Ordinal.card_iSup_Iio_le_sum_card
View on Github →