Commit 2024-12-12 22:51 d554797d
View on Github →chore(SetTheory/Cardinal/Arithmetic): generalize card_iSup_Iio_le_sum_card (#19727)
The theorem becomes strictly more general at zero cost by letting the domain of the function be Iio o rather than Ordinal.