Theorems · Definition · measure theory

MeasureTheory.VectorMeasure.Integrable

{X : Type u_2} →
  {E : Type u_4} →
    {F : Type u_5} →
      {mX : MeasurableSpace X} →
        [NormedAddCommGroup E] → [inst : NormedAddCommGroup F] → MeasureTheory.VectorMeasure X F → (X → E) → Prop

f : X → E is said to be integrable with respect to μ and B if it is integrable with respect to (μ.transpose B).variation.

Defined in

Mathlib.MeasureTheory.VectorMeasure.Integral

Cited by

63 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedAddCommGroup