piContent_eq_infinitePiNat — Mathlib

English

For cylinders A that are measurable, piContent μ A equals infinitePiNat μ A; i.e., the content of a cylinder under the pi-content matches the corresponding infinite product construction.

Русский

Для цилиндров A, являющихся измеримыми, piContent μ A равно infinitePiNat μ A; содержательное значение цилиндра соответствует бесконечному произведению.

LaTeX

$$$$\piContent\,\mu\,A = \mathrm{infinitePiNat}\,\mu\,A.$$$$

Lean4

theorem piContent_eq_infinitePiNat {A : Set (Π n, X n)} (hA : A ∈ measurableCylinders X) :
    piContent μ A = infinitePiNat μ A :=
  by
  obtain ⟨s, S, mS, rfl⟩ : ∃ s S, MeasurableSet S ∧ A = cylinder s S := by simpa [mem_measurableCylinders] using hA
  rw [piContent_cylinder _ mS, cylinder, ← map_apply (measurable_restrict _) mS, infinitePiNat_map_restrict]

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