∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {𝒢 : MeasureTheory.Filtration ℕ m0} [inst_3 : PartialOrder E]
  [IsOrderedAddMonoid E] [ClosedIciTopology E] [IsOrderedModule ℝ E] [MeasureTheory.IsFiniteMeasure μ] {f : ℕ → Ω → E},
  MeasureTheory.StronglyAdapted 𝒢 f →
    (∀ (i : ℕ), MeasureTheory.Integrable (f i) μ) →
      (∀ (i : ℕ), 0 ≤ᵐ[μ] μ[f (i + 1) - f i | ↑𝒢 i]) → MeasureTheory.Submartingale f 𝒢 μ