volume_Icc_pi — Mathlib

English

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

Русский

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

LaTeX

$$$\operatorname{volume}(Icc a b) = \prod i, ENNReal.ofReal (b_i - a_i)$$$

Lean4

theorem volume_Icc_pi {a b : ι → ℝ} : volume (Icc a b) = ∏ i, ENNReal.ofReal (b i - a i) :=
  by
  rw [← pi_univ_Icc, volume_pi_pi]
  simp only [Real.volume_Icc]

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