mathlib3

49fc7edd - feat(measure_theory): assorted integration lemmas (#4145)

feat(measure_theory): assorted integration lemmas (#4145) from the sphere eversion project This is still preparations for differentiation of integals depending on a parameter.