Commit 2024-08-28 11:38 79ef7496

View on Github →

feat: a finite sum of finite measures is finite (#16213) From LeanAPAP

Estimated changes

Modified Mathlib/Data/ENNReal/Operations.lean

modified theorem ENNReal.sum_eq_top

modified theorem ENNReal.sum_lt_top

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean