Theorem MeasureTheory.setLIntegral_le_meas

Modification history

2025-04-15 05:27

Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean

chore: split `MeasureTheory.Integral.Lebesgue.Basic` (#23860) …

Modified MeasureTheory.setLIntegral_le_meas View on Github →

2024-10-09 19:21

Mathlib/MeasureTheory/Integral/Lebesgue.lean

feat: `setLintegral` for indicator function and `le_meas` (#15322) …

Added MeasureTheory.setLIntegral_le_meas View on Github →