ι : Type u_1
inst✝ : Fintype ι
a b : ι → ℝ
⊢ ∏ i : ι, ↑↑volume (Icc (a i) (b i)) = ∏ i : ι, ofReal (b i - a i)
ι : Type u_1
inst✝ : Fintype ι
a b : ι → ℝ
⊢ ↑↑volume (Icc a b) = ∏ i : ι, ofReal (b i - a i)
rw [← pi_univ_Icc, volume_pi_pi]
no goals
ι : Type u_1
inst✝ : Fintype ι
a b : ι → ℝ
⊢ ∏ i : ι, ↑↑volume (Icc (a i) (b i)) = ∏ i : ι, ofReal (b i - a i)
simp only [Real.volume_Icc]