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