mathlib
mathlib copied to clipboard
feat(measure_theory/integral/lebesgue): add a lemma
A lintegral
version of a lemma from @sgouezel's #13690.
- [x] depends on: #14293
- [x] depends on: #14294
- [x] depends on: #14296
This PR/issue depends on:
- ~~leanprover-community/mathlib#14293~~
- ~~leanprover-community/mathlib#14294~~
- ~~leanprover-community/mathlib#14296~~ By Dependent Issues (🤖). Happy coding!
Looks like this is broken as you removed lintegral_add'
in another PR so I'm removing awaiting review for now