Theorem Ordinal.lift_card_iSup_le_sum_card

Modification history

2026-05-10 09:03
Mathlib/SetTheory/Cardinal/Ordinal.lean
feat: supremum of `≤ c` ordinals of cardinal `≤ c` has cardinal `≤ c` (#37573)
Modified Ordinal.lift_card_iSup_le_sum_cardView on Github →
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 →