Commit 2021-07-05 17:24 b6bf7a30
View on Github →feat(measure_theory/lp_space): define the Lp function corresponding to the indicator of a set (#8193) I also moved some measurability lemmas from the integrable_on file to measure_space. I needed them and lp_space is before integrable_on in the import graph.