∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F}
  {ι : Sort u_4} [Countable ι] {s : ι → Set α}, (μ (⋃ i, s i) = 0) = ∀ (i : ι), μ (s i) = 0