∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (i : Set α),
  MeasurableSet i →
    ∀ (hi₂ : MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i),
      s.toMeasureOfZeroLE' i hi₂ ∅ ⋯ = 0