∀ {X : Type u_1} [inst : MeasurableSpace X] (f : Set X → ENNReal) {s₁ s₂ : Set X} (hs₁ : MeasurableSet s₁),
  MeasurableSet s₂ → s₁ ⊆ s₂ → ∀ (P : Finpartition ⟨s₁, hs₁⟩), ∑ p ∈ P.parts, f ↑p ≤ MeasureTheory.preVariationFun f s₂