Commit 2021-06-23 21:01 3cf80395

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.