volume_apply — Mathlib

English

For any box I and any vector x in E, BoxAdditiveMap.volume I x = (∏ j (I.upper j − I.lower j)) · x.

Русский

Для коробки I и вектора x в E выполняется BoxAdditiveMap.volume I x = (∏_j (I.upper_j − I.lower_j)) · x.

LaTeX

$$$BoxAdditiveMap.volume(I)\\,x = \\Big(\\prod_{j} (I.upper j - I.lower j)\\Big) \\cdot x$$$

Lean4

theorem volume_apply {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (I : Box ι) (x : E) :
    BoxAdditiveMap.volume I x = (∏ j, (I.upper j - I.lower j)) • x :=
  by
  rw [BoxAdditiveMap.volume, toSMul_apply]
  exact congr_arg₂ (· • ·) I.volume_apply rfl

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