measure_cylinder — Mathlib

English

If μ is a projective limit of P, then for any I and measurable s, μ(cylinder I s) = P I s.

Русский

Если μ является проективным пределом P, то для любого I и измеримого s верно μ(cylinder I s) = P I s.

LaTeX

$$$\text{If } h:\ IsProjectiveLimit \mu P,\ I:Finset ι,\ s: Set(Π i: I, α i),\ hs:\ MeasurableSet s,\ \mu(\mathrm{cylinder}(I,s)) = P I s.$$$

Lean4

theorem measure_cylinder (h : IsProjectiveLimit μ P) (I : Finset ι) {s : Set (∀ i : I, α i)} (hs : MeasurableSet s) :
    μ (cylinder I s) = P I s := by
  rw [cylinder, ← Measure.map_apply _ hs, h I]
  exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _)

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