2023-01-31 19:36
src/measure_theory/integral/peak_function.lean
feat(measure_theory/integral/peak_function): convergence of integral against a sequence of peak functions (#18327) …
Added integrable_on_peak_smul_of_integrable_on_of_continuous_within_at