mathlib

8b93d3a5 - feat(measure_theory/function/lp_space): generalize some `integrable` lemmas to `mem_ℒp` (#11231)

feat(measure_theory/function/lp_space): generalize some `integrable` lemmas to `mem_ℒp` (#11231) I would like to define integrable as `mem_ℒp` for `p = 1` and remove the `has_finite_integral` prop. But first we need to generalize everything we have about `integrable` to `mem_ℒp`. This is one step towards that goal.