no goals
α : Type u_2
β : Type ?u.30962
γ : Type ?u.30965
δ : Type ?u.30968
δ' : Type ?u.30971
ι✝ : Sort ?u.30974
s✝ t u : Set α
ι : Sort u_1
m : ι → MeasurableSpace α
s : Set α
⊢ MeasurableSet s ↔ ∀ (i : ι), MeasurableSet s
rw [iInf, measurableSet_sInf, forall_range_iff]