∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s →
    μ.restrict s ≤ ν.restrict s → ν.restrict sᶜ ≤ μ.restrict sᶜ → MeasureTheory.IsHahnDecomposition μ ν s