volume_pi_closedBall — Mathlib

English

Let ι be finite and a : ι → ℝ. For r ≥ 0, the Lebesgue volume of the product of closed balls equals ENNReal.ofReal ((2 · r)^{|ι|}).

Русский

Пусть ι конечен и a : ι → ℝ. Для r ≥ 0 объём произведения круглых шаров равен ENNReal.ofReal ((2 · r)^{|ι|}).

LaTeX

$$$$ \\mathrm{volume}(\\mathrm{Metric.closedBall}\\ a\\ r) = \\mathrm{ENNReal.ofReal}((2 \\cdot r)^{|\\iota|}). $$$$

Lean4

@[simp]
nonrec theorem volume_pi_closedBall (a : ι → ℝ) {r : ℝ} (hr : 0 ≤ r) :
    volume (Metric.closedBall a r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι) :=
  by
  simp only [MeasureTheory.volume_pi_closedBall a hr, volume_closedBall, Finset.prod_const]
  exact (ENNReal.ofReal_pow (mul_nonneg zero_le_two hr) _).symm

Похожие утверждения