Theorem MeasureTheory.laverage_mono_ae

Modification history

2026-06-07 02:12
Mathlib/MeasureTheory/Integral/Average.lean
feat(GRewrite): new `grw` implementation (#38318) …
Modified MeasureTheory.laverage_mono_aeView on Github →
2026-04-07 13:03
Mathlib/MeasureTheory/Integral/Average.lean
feat(MeasureTheory/Integral/Average): add `laverage_mono_ae` and `setLAverage_le_essSup` (#37551) …
Added MeasureTheory.laverage_mono_aeView on Github →