mathlib

74a0f67b - refactor(measure_theory/simple_func_dense): generalize approximation results from L^1 to L^p (#8114)

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.