mathlib

3cf80395 - feat(measure_theory/set_integral): the set integral is continuous (#7931)

feat(measure_theory/set_integral): the set integral is continuous (#7931) Most of the code is dedicated to building a continuous linear map from Lp to the Lp space corresponding to the restriction of the measure to a set. The set integral is then continuous as composition of the integral and that map.