volume_pi_Ico_toReal — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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