∀ {α : Type u_1} {ι : Type u_8} {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) {As : ι → Set α},
  (∀ (i : ι), MeasurableSet (As i)) → Pairwise (Function.onFun Disjoint As) → ∑' (i : ι), μ (As i) ≤ μ (⋃ i, As i)