Theorems · Definition · measure theory

MeasureTheory.weightedSMul

{α : Type u_1} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup F] →
      [inst_1 : NormedSpace ℝ F] → {x : MeasurableSpace α} → MeasureTheory.Measure α → Set α → F →L[ℝ] F

Given a set s, return the continuous linear map fun x => μ.real s • x. The extension of that set function through setToL1 gives the Bochner integral of L1 functions.

Defined in

Mathlib.MeasureTheory.Integral.Bochner.L1

Cited by

31 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace