Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes