Theorems · Definition · measure theory

MeasureTheory.L1.SimpleFunc.integral

{α : Type u_1} →
  {E : Type u_2} →
    [inst : NormedAddCommGroup E] →
      {m : MeasurableSpace α} → {μ : MeasureTheory.Measure α} → [NormedSpace ℝ E] → ↥(α →₁ₛ[μ] E) → E

The Bochner integral over simple functions in L1 space.

Defined in

Mathlib.MeasureTheory.Integral.Bochner.L1

Cited by

12 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace