Theorem MeasureTheory.eLpNorm'_eq_lintegral_nnnorm

Modification history

2024-12-23 14:32
Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
feat: generalize measure-theoretic definitions using ENorm (#20122) …
Added MeasureTheory.eLpNorm'_eq_lintegral_nnnormView on Github →