Theorem MeasureTheory.Integrable.smul_bdd

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.smul_bddView on Github →