ι : Type u_1
I : Box ι
inst✝ : Countable ι
⊢ MeasurableSet (pi univ fun i => Ioc (lower I i) (upper I i))
ι : Type u_1
I : Box ι
inst✝ : Countable ι
⊢ MeasurableSet ↑I
rw [coe_eq_pi]
no goals
ι : Type u_1
I : Box ι
inst✝ : Countable ι
⊢ MeasurableSet (pi univ fun i => Ioc (lower I i) (upper I i))
exact MeasurableSet.univ_pi fun i => measurableSet_Ioc