Commit 2026-05-14 11:38 28908c09

View on Github →

chore: remove assumption in exist_eLpNorm_sub_le_of_continuous (#39354)

Estimated changes

Modified Mathlib/Analysis/Normed/Lp/SmoothApprox.lean

modified theorem HasCompactSupport.exist_eLpNorm_sub_le_of_continuous