Theorem Ordinal.lift_card_iSup_le_sum_card

Modification history

2025-03-17 11:54
Mathlib/SetTheory/Cardinal/Arithmetic.lean
refactor(SetTheory/Cardinal/Ordinal): move results (#21857) …
Modified Ordinal.lift_card_iSup_le_sum_cardView 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.lift_card_iSup_le_sum_cardView on Github →