Theorem MeasureTheory.memLp_enorm_rpow_iff

Modification history

2025-05-12 15:41
Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
refactor(LpSeminorm/Basic, LpSpace/Basic): generalise more lemmas to enorms (#24640) …
Added MeasureTheory.memLp_enorm_rpow_iffView on Github →