Theorem MeasureTheory.laverage_le_essSup

Modification history

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_le_essSup View on Github →