Theorem HasCompactSupport.ennnorm_le_lintegral_Ici_deriv

Modification history

2024-06-29 17:35
Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
feat: remove completeness assumption in Sobolev inequality (#14262)
Added HasCompactSupport.ennnorm_le_lintegral_Ici_derivView on Github →