Theorems · Theorem · measure theory

Continuous.memLp_of_hasCompactSupport

∀ {E : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup E] {X : Type u_3} [inst_1 : TopologicalSpace X]
  [inst_2 : MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasureOnCompacts μ]
  [OpensMeasurableSpace X] {f : X → E}, Continuous f → HasCompactSupport f → MeasureTheory.MemLp f p μ

A continuous function with compact support is in L^p.

Defined in

Mathlib.MeasureTheory.Function.LpSpace.Indicator

Cited by

2 results in Mathlib

Foundations

Depth 215 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupTopologicalSpaceMeasurableSpaceMeasureTheory.IsFiniteMeasureOnCompactsOpensMeasurableSpace