mathlib3

a8c97ed3 - feat(measure_theory/function/continuous_map_dense): compactly supported functions are dense in L^p (#18710)

feat(measure_theory/function/continuous_map_dense): compactly supported functions are dense in L^p (#18710) We have already the fact that bounded continuous functions are dense in L^p. We refactor the proof to extract an approach that is common to bounded continuous functions and to compactly supported functions, to avoid code duplication as much as possible. We also give elementary versions of the statements (in the form: for all epsilon > 0, there exists g such that...) as they may be easier to use, and specialized versions for integrable functions. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>