feat(MeasureTheory/LpSpace): add ContinuousMap.memLp (leanprover-community#37560)

Add `ContinuousMap.memLp`: a continuous function on a compact space is in L^p.

Upstreamed from the [Carleson](https://github.com/fpvandoorn/carleson) project.

Co-authored-by: Leo Diedering <129694072+ldiedering@users.noreply.github.com>

Author: pitmonticone

Mathlib/MeasureTheory/Function/LpSpace/ContinuousFunctions.lean

@@ -14,7 +14,7 @@ public import Mathlib.Topology.ContinuousMap.Compact
 # Continuous functions in Lp space
 
 When `α` is a topological space equipped with a finite Borel measure, there is a bounded linear map
-from the normed space of bounded continuous functions (`α →ᵇ E`) to `Lp E p μ`.  We construct this
+from the normed space of bounded continuous functions (`α →ᵇ E`) to `Lp E p μ`. We construct this
 as `BoundedContinuousFunction.toLp`.
 
 -/
@@ -207,4 +207,9 @@ theorem toLp_norm_le :
   rw [toLp_norm_eq_toLp_norm_coe]
   exact BoundedContinuousFunction.toLp_norm_le μ
 
+lemma memLp (𝕜' : Type*) [NormedField 𝕜'] [NormedSpace 𝕜' E] (f : C(α, E)) :
+    MemLp f p μ := by
+  have := Lp.mem_Lp_iff_memLp.mp (Subtype.val_prop (f.toLp p μ 𝕜'))
+  rwa [coe_toLp, memLp_congr_ae (coeFn_toAEEqFun _ _)] at this
+
 end ContinuousMap