Theorems · Theorem · functional analysis

MeasureTheory.Lp.coeFn_smul

∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedRing 𝕜] [inst_2 : Module 𝕜 E] [inst_3 : IsBoundedSMul 𝕜 E] (c : 𝕜)
  (f : ↥(MeasureTheory.Lp E p μ)), ↑↑(c • f) =ᵐ[μ] c • ↑↑f

Defined in

Mathlib.MeasureTheory.Function.LpSpace.Basic

Cited by

11 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedRingModuleIsBoundedSMul