volume_apply' — Mathlib

English

The real-valued volume of a box I is the product of its side-lengths: ((volume) I).toReal = ∏ i (I.upper i − I.lower i).

Русский

Действительное значение объёма коробки I равно произведению длин его сторон: ((volume) I).toReal = ∏_i (I.upper i − I.lower i).

LaTeX

$$$((\\text{volume} : \\text{Measure}(\\iota \\to \\mathbb{R})) I).toReal = \\prod_{i} (I.upper i - I.lower i)$$$

Lean4

@[simp]
theorem volume_apply' (I : Box ι) : ((volume : Measure (ι → ℝ)) I).toReal = ∏ i, (I.upper i - I.lower i) := by
  rw [coe_eq_pi, Real.volume_pi_Ioc_toReal I.lower_le_upper]

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