piContent_cylinder — Mathlib

English

The content of a cylinder built from a finite index set I and a measurable base S equals the content of the corresponding product measure on S.

Русский

Содержимое цилиндра, построенного по конечному набору индексов I и измеримому базису S, равно содержанию произведения мер на S.

LaTeX

$$$\text{piContent } μ (\text{cylinder } I\ S) = \text{Measure.pi } (fun i:\, I ↦ μ i) S$$$

Lean4

theorem piContent_cylinder {I : Finset ι} {S : Set (Π i : I, X i)} (hS : MeasurableSet S) :
    piContent μ (cylinder I S) = Measure.pi (fun i : I ↦ μ i) S :=
  projectiveFamilyContent_cylinder _ hS

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