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