Theorems · Definition · measure theory

MeasureTheory.Lp.simpleFunc.coeToLp

(α : Type u_1) →
  (E : Type u_4) →
    (𝕜 : Type u_6) →
      [inst : MeasurableSpace α] →
        [inst_1 : NormedAddCommGroup E] →
          {p : ENNReal} →
            {μ : MeasureTheory.Measure α} →
              [inst_2 : Fact (1 ≤ p)] →
                [inst_3 : NormedRing 𝕜] →
                  [inst_4 : Module 𝕜 E] →
                    [inst_5 : IsBoundedSMul 𝕜 E] → ↥(MeasureTheory.Lp.simpleFunc E p μ) →L[𝕜] ↥(MeasureTheory.Lp E p μ)

The embedding of Lp simple functions into Lp functions, as a continuous linear map.

Defined in

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Cited by

5 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceNormedAddCommGroupFactNormedRingModuleIsBoundedSMul