mathlib

7e109c4b - feat(measure_theory/lp_space): continuous functions on compact space are in Lp (#6919)

feat(measure_theory/lp_space): continuous functions on compact space are in Lp (#6919) Continuous functions on a compact space equipped with a finite Borel measure are in Lp, and the inclusion is a bounded linear map. This follows directly by transferring the construction in #6878 for bounded continuous functions, using the fact that continuous function on a compact space are bounded.