Commit 2021-07-03 13:08 74a0f67b

refactor(measure_theory/simple_func_dense): generalize approximation results from L^1 to L^p (#8114) Simple functions are dense in L^p. The argument for 1 ≤ p < ∞ is exactly the same as for p = 1, which was already in mathlib: construct a suitable sequence of pointwise approximations and apply the Dominated Convergence Theorem. This PR refactors to provide the general-p result. The argument for p = ∞ requires finite-dimensionality of E and a different approximating sequence, so is left for another PR.