Theorems · Definition · measure theory

MeasureTheory.Lp.simpleFunc.module

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

If E is a normed space, Lp.simpleFunc E p μ is a module. Not declared as an instance as it is (as of writing) used only in the construction of the Bochner integral.

Defined in

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Cited by

29 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceNormedAddCommGroupNormedRingModuleIsBoundedSMul