Theorem MeasureTheory.eLpNorm_dirac

Modification history

2026-03-06 09:14
Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean
feat: lemmas about `Measure.count` (#36205) …
Added MeasureTheory.eLpNorm_diracView on Github →