Theorem MeasureTheory.SimpleFunc.setToSimpleFunc_eq_sum_of_subset

Modification history

2026-06-19 10:05
Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
chore: move strong measurability proof to `setToFun` (#40602) …
Added MeasureTheory.SimpleFunc.setToSimpleFunc_eq_sum_of_subsetView on Github →