Theorems · Theorem · measure theory

MeasureTheory.SimpleFunc.memLp_approxOn

∀ {β : Type u_2} {E : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace E] [inst_2 : NormedAddCommGroup E]
  {p : ENNReal} [inst_3 : BorelSpace E] {f : β → E} {μ : MeasureTheory.Measure β} (fmeas : Measurable f),
  MeasureTheory.MemLp f p μ →
    ∀ {s : Set E} {y₀ : E} (h₀ : y₀ ∈ s) [inst_4 : TopologicalSpace.SeparableSpace ↑s],
      MeasureTheory.MemLp (fun x => y₀) p μ →
        ∀ (n : ℕ), MeasureTheory.MemLp (⇑(MeasureTheory.SimpleFunc.approxOn f fmeas s y₀ h₀ n)) p μ

Defined in

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpaceNormedAddCommGroupBorelSpaceTopologicalSpace.SeparableSpace