volume_Icc_pi_toReal — Mathlib

English

If a ≤ b then the real-valued volume of Icc(a,b) equals the product ∏i (b_i − a_i).

Русский

Пусть a ≤ b; тогда действительный объем Icc(a,b) равен произведению длин ∏i (b_i − a_i).

LaTeX

$$$\text{(a \le b)} \Rightarrow (\operatorname{volume}(Icc a b)).\toReal = \prod i (b_i - a_i)$$$

Lean4

@[simp]
theorem volume_Icc_pi_toReal {a b : ι → ℝ} (h : a ≤ b) : (volume (Icc a b)).toReal = ∏ i, (b i - a i) := by
  simp only [volume_Icc_pi, ENNReal.toReal_prod, ENNReal.toReal_ofReal (sub_nonneg.2 (h _))]

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