∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] {C : ℝ},
  (∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C) →
    ∀ {s : Set X},
      MeasurableSet s → MeasureTheory.Integrable f μ → ‖∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ‖ ≤ μ.real sᶜ * C