Theorem MeasureTheory.Integrable.bdd_smul

Modification history

2025-11-26 16:01
Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
feat: many lemmas on integrability of a bounded linear map composed with two functions (#31661) …
Added MeasureTheory.Integrable.bdd_smulView on Github →