∀ {α : Type u_1} [inst : MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal} (m0 : m ∅ ⋯ = 0),
  (∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
      Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) →
    ∀ {s : Set α}, MeasurableSet s → (MeasureTheory.inducedOuterMeasure m ⋯ m0) s = MeasureTheory.extend m s