volume_pi_Ioc_toReal — Mathlib

English

Let a,b : ι → ℝ with a ≤ b. Then the real-valued volume (toReal) of the product ∏_{i} Ioc(a_i,b_i) equals ∏_{i} (b_i − a_i).

Русский

Пусть a,b : ι → ℝ с a_i ≤ b_i. Тогда действительный объём (toReal) произведения ∏_{i} Ioc(a_i,b_i) равен ∏_{i} (b_i − a_i).

LaTeX

$$$$ (\\mathrm{volume}( \\pi_{i \\in \\mathrm{univ}} Ioc(a_i,b_i) ))^{\\toReal} = \\prod_i (b_i - a_i). $$$$

Lean4

@[simp]
theorem volume_pi_Ioc_toReal {a b : ι → ℝ} (h : a ≤ b) :
    (volume (pi univ fun i => Ioc (a i) (b i))).toReal = ∏ i, (b i - a i) := by
  simp only [volume_pi_Ioc, ENNReal.toReal_prod, ENNReal.toReal_ofReal (sub_nonneg.2 (h _))]

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