volume_pi_Ioo — Mathlib

English

Let a,b: ι → ℝ with finite ι. The volume of the Cartesian product π univ of open intervals Ioo(a_i,b_i) equals the product ∏i ENNReal.ofReal(b_i − a_i).

Русский

Пусть a,b:ι→ℝ; объём произведения Ioo(a_i,b_i) по индексу i равен произведению ENNReal.ofReal(b_i − a_i).

LaTeX

$$$\operatorname{volume}(\pi univ fun i => Ioo (a i) (b i)) = \prod i, ENNReal.ofReal (b i - a i)$$$

Lean4

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

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