Theorem MeasureTheory.Memℒp.mono_exponent

Modification history

2025-01-13 10:56
Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean
chore(LpSpace): move results about the L^p norm earlier (#20541) …
Added MeasureTheory.Memℒp.mono_exponentView on Github →