ι : Type u_1
I : Box ι
inst✝ : Fintype ι
⊢ (pi univ fun i => Ioc (lower I i) (upper I i)) =ᵐ[volume] ↑Box.Icc I
ι : Type u_1
I : Box ι
inst✝ : Fintype ι
⊢ ↑I =ᵐ[volume] ↑Box.Icc I
rw [coe_eq_pi]
no goals
ι : Type u_1
I : Box ι
inst✝ : Fintype ι
⊢ (pi univ fun i => Ioc (lower I i) (upper I i)) =ᵐ[volume] ↑Box.Icc I
exact Measure.univ_pi_Ioc_ae_eq_Icc