ι : Type u_1
inst✝ : Fintype ι
a : ι → ℝ
r : ℝ
hr : 0 ≤ r
⊢ ofReal (2 * r) ^ Finset.card Finset.univ = ofReal ((2 * r) ^ Fintype.card ι)
ι : Type u_1
inst✝ : Fintype ι
a : ι → ℝ
r : ℝ
hr : 0 ≤ r
⊢ ↑↑volume (Metric.closedBall a r) = ofReal ((2 * r) ^ Fintype.card ι)
simp only [MeasureTheory.volume_pi_closedBall a hr, volume_closedBall, Finset.prod_const]
no goals
ι : Type u_1
inst✝ : Fintype ι
a : ι → ℝ
r : ℝ
hr : 0 ≤ r
⊢ ofReal (2 * r) ^ Finset.card Finset.univ = ofReal ((2 * r) ^ Fintype.card ι)
exact (ENNReal.ofReal_pow (mul_nonneg zero_le_two hr) _).symm