theorem HasCompactSupport.memLp_of_enorm_bound {E : Type u_2} {p : ENNReal} [NormedAddCommGroup E] {X : Type u_3} [TopologicalSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {f : X → E} (hf : HasCompactSupport f) (h2f : MeasureTheory.AEStronglyMeasurable f μ) {C : ENNReal} (hfC : ∀ᵐ (x : X) ∂μ, ‖f x‖ₑ ≤ C) (hC : C ≠ ⊤) : MeasureTheory.MemLp f p μ

A bounded measurable function with compact support is in L^p.