Theorem Ordinal.card_iSup_Iio_le_card_mul_iSup

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_card_mul_iSupView 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_card_mul_iSupView 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_card_mul_iSupView on Github →