Theorem MeasureTheory.memℒp_of_bounded

Modification history

2024-10-21 10:47
Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
feat: Popoviciu's inequality (#17868) …
Added MeasureTheory.memℒp_of_boundedView on Github →