volume_pi_Ioc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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