volume_pi_Ioo_toReal — Mathlib

English

Let ι be a finite index set. For functions a,b : ι → ℝ with a_i ≤ b_i for all i, the Lebesgue volume of the Cartesian product ∏_{i∈ι} Ioo(a_i,b_i) equals ∏_{i∈ι} (b_i − a_i).

Русский

Пусть ι – конечное множество индексов. Пусть a,b : ι → ℝ такие, что для всех i выполняется a_i ≤ b_i. Объём Лебега множества ∏_{i∈ι} Ioo(a_i,b_i) равен ∏_{i∈ι} (b_i − a_i).

LaTeX

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

Lean4

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

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