Commit 2024-11-13 17:52 5659e13f

View on Github →

feat(SetTheory/Cardinal/Ordinal): sum_eq_iSup (#16910) Prove sum_eq_iSup, an infinite sum is equal to the supremum of summands.

Estimated changes

added theorem Cardinal.sum_eq_iSup