Theorems · Theorem · measure theory

MeasureTheory.Lp.simpleFunc.smul_toSimpleFunc

∀ {α : 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] [inst_4 : IsBoundedSMul 𝕜 E] (k : 𝕜)
  (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)),
  ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc (k • f)) =ᵐ[μ] k • ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)

Defined in

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceNormedAddCommGroupNormedRingModuleIsBoundedSMul