Theorem MeasureTheory.eLpNormEssSup_eq_essSup_nnnorm

Modification history

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