Theorem ENNReal.ofReal_essSup

Modification history

2026-02-09 07:29
Mathlib/MeasureTheory/Function/EssSup.lean
feat: real-valued Lᵖ norm (#23881)
Added ENNReal.ofReal_essSupView on Github →