volume_Iio — Mathlib

English

For finite index set ι and intervals Icc(a_i,b_i), the volume of the Cartesian product ∏i Icc(a_i,b_i) equals the product ∏i ENNReal.ofReal(b_i−a_i).

Русский

Для конечного множества индексов ι и интервалов Icc(a_i,b_i), объем произведения ∏i Icc(a_i,b_i) равен произведению ∏i ENNReal.ofReal(b_i−a_i).

LaTeX

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

Lean4

@[simp]
theorem volume_Iio {a : ℝ} : volume (Iio a) = ∞ :=
  top_unique <|
    le_of_tendsto' ENNReal.tendsto_nat_nhds_top fun n =>
      calc
        (n : ℝ≥0∞) = volume (Ioo (a - n) a) := by simp
        _ ≤ volume (Iio a) := measure_mono Ioo_subset_Iio_self

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