Theorem Ordinal.card_iSup_le_lift

Modification history

2026-05-10 09:03
Mathlib/SetTheory/Cardinal/Ordinal.lean
feat: supremum of `≤ c` ordinals of cardinal `≤ c` has cardinal `≤ c` (#37573)
Added Ordinal.card_iSup_le_liftView on Github →