no goals
ι : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t✝ u v : Set α
inst✝ : Countable ι
t : ι → Set α
⊢ AEDisjoint μ s (⋃ (i : ι), t i) ↔ ∀ (i : ι), AEDisjoint μ s (t i)
simp only [AEDisjoint, inter_iUnion, measure_iUnion_null_iff]