Commit 2024-07-15 08:20 08bbfd6e

View on Github →

feat(Topology/ENNReal): add finset_sum_iSup (#14738) Moves:

finset_sum_iSup_nat -> finsetSum_iSup_of_monotone

Estimated changes

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

Modified Mathlib/Topology/Instances/ENNReal.lean

added theorem ENNReal.finsetSum_iSup

added theorem ENNReal.finsetSum_iSup_of_monotone

deleted theorem ENNReal.finset_sum_iSup_nat

modified theorem ENNReal.iSup_add_iSup_of_monotone