{Ω : Type u_1} →
  {E : Type u_2} →
    {ι : Type u_3} →
      [inst : Preorder ι] →
        {m0 : MeasurableSpace Ω} →
          [inst_1 : NormedAddCommGroup E] →
            [NormedSpace ℝ E] →
              [CompleteSpace E] → [LE E] → (ι → Ω → E) → MeasureTheory.Filtration ι m0 → MeasureTheory.Measure Ω → Prop