volume_pi_pi — Mathlib

English

For finite index set, the volume of a product of sets s_i equals the product of volumes of each s_i.

Русский

Объем произведения множеств s_i равен произведению объёмов каждого s_i.

LaTeX

$$$volume(\pi univ\, s) = \prod_i volume(s_i)$$$

Lean4

theorem volume_pi_pi [∀ i, MeasureSpace (α i)] [∀ i, SigmaFinite (volume : Measure (α i))] (s : ∀ i, Set (α i)) :
    volume (pi univ s) = ∏ i, volume (s i) :=
  Measure.pi_pi (fun _ => volume) s

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