Theorem MeasureTheory.SimpleFunc.setToSimpleFunc_eq_sum_filter
Modification history
2025-04-15 10:46
Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
chore: split `MeasureTheory.Integral.SetToL1` (#24075) …
Modified MeasureTheory.SimpleFunc.setToSimpleFunc_eq_sum_filterView on Github →