volume_box — Mathlib

English

The volume of box n ν equals 1/n^{card ι}, independent of ν.

Русский

Объем коробки box(n,ν) равен 1/n^{card ι}, не зависит от ν.

LaTeX

$$$\operatorname{volume}(box(n,ν)) = \frac{1}{n^{\operatorname{card}}(ι)}$$$

Lean4

@[simp]
theorem volume_box (ν : ι → ℤ) : volume (box n ν : Set (ι → ℝ)) = 1 / n ^ card ι := by
  simp_rw [volume_pi, BoxIntegral.Box.coe_eq_pi, Measure.pi_pi, Real.volume_Ioc, box.upper_sub_lower, Finset.prod_const,
    ENNReal.ofReal_div_of_pos (Nat.cast_pos.mpr n.pos_of_neZero), ENNReal.ofReal_one, ENNReal.ofReal_natCast, one_div,
    ENNReal.inv_pow, Finset.card_univ]

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