volume_pi_Ico — Mathlib

English

Let ι be finite and a,b : ι → ℝ. The Lebesgue volume of the product ∏_{i} Ico(a_i,b_i) equals ∏_{i} ENNReal.ofReal(b_i − a_i).

Русский

Пусть ι конечен, а,b : ι → ℝ. Объём произведения ∏_{i} Ico(a_i,b_i) равен ∏_{i} ENNReal.ofReal(b_i − a_i).

LaTeX

$$$$ \\mathrm{volume}\\biggl( \\pi_{i \\in \\mathrm{univ}} Ico(a_i,b_i)\\biggr) = \\prod_i \\mathrm{ENNReal.ofReal}(b_i - a_i). $$$$

Lean4

theorem volume_pi_Ico {a b : ι → ℝ} : volume (pi univ fun i => Ico (a i) (b i)) = ∏ i, ENNReal.ofReal (b i - a i) :=
  (measure_congr Measure.univ_pi_Ico_ae_eq_Icc).trans volume_Icc_pi

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