Theorems · Definition · measure theory

MeasureTheory.L1.integral

{α : Type u_5} →
  {E : Type u_6} →
    [inst : NormedAddCommGroup E] →
      {m : MeasurableSpace α} →
        {μ : MeasureTheory.Measure α} → [NormedSpace ℝ E] → [CompleteSpace E] → ↥(MeasureTheory.Lp E 1 μ) → E

The Bochner integral in L1 space

Defined in

Mathlib.MeasureTheory.Integral.Bochner.L1

Cited by

27 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace