mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

feat(measure_theory/integral/lebesgue): add a lemma

Open urkud opened this issue 2 years ago • 2 comments

A lintegral version of a lemma from @sgouezel's #13690.


  • [x] depends on: #14293
  • [x] depends on: #14294
  • [x] depends on: #14296

Open in Gitpod

urkud avatar May 22 '22 01:05 urkud

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

alexjbest avatar Oct 07 '22 00:10 alexjbest