∀ {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} (s : Set α),
  (∀ ⦃t : Set α⦄, s ⊆ t → m s ≤ m t) →
    (∀ (s : ℕ → Set α), m (⋃ i, s i) ≤ ∑' (i : ℕ), m (s i)) → (MeasureTheory.OuterMeasure.ofFunction m m_empty) s = m s