infinitePi_cylinder — Mathlib

English

IsProjectiveLimit on cylinders: the value on cylinder S equals the product across indices.

Русский

IsProjectiveLimit на цилиндрах: значение на цилиндре равно произведению по индексам.

LaTeX

$$$$\mathrm{infinitePi}(μ)(\text{cylinder } s S) = \prod_{i \in s} μ_i(S_i).$$$$

Lean4

theorem infinitePi_cylinder {s : Finset ι} {S : Set (Π i : s, X i)} (mS : MeasurableSet S) :
    infinitePi μ (cylinder s S) = Measure.pi (fun i : s ↦ μ i) S := by
  rw [cylinder, ← Measure.map_apply (measurable_restrict _) mS, infinitePi_map_restrict]

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