Theorem ENNReal.LpAddConst_ne_zero

Modification history

2026-09-11 14:45
Mathlib/Analysis/MeanInequalitiesPow.lean
refactor(MeasureTheory): define `eLpNorm f` to be infinite when not `AEStronglyMeasurable` (#42406) …
Added ENNReal.LpAddConst_ne_zeroView on Github →