pi_eq_generateFrom_projections — Mathlib

English

The product σ-algebra on a family of spaces equals the σ-algebra generated by the preimages of measurable sets under coordinate projections.

Русский

Произведение σ-алгебр равно σ-алгебре, генерируемой предобразами измеримых множеств по координатным проекциям.

LaTeX

$$$\\mathrm{pi} = \\mathrm{generateFrom}\\{B : \\text{Set }(\\alpha_i) \\mid \\exists i,A\\,(\\mathrm{MeasurableSet}(A) \\land \\mathrm{preimage}(\\mathrm{eval}_i,A)=B)\\}$$$

Lean4

theorem pi_eq_generateFrom_projections {mα : ∀ i, MeasurableSpace (α i)} :
    pi = generateFrom {B | ∃ (i : ι) (A : Set (α i)), MeasurableSet A ∧ eval i ⁻¹' A = B} := by
  simp only [pi, ← generateFrom_iUnion_measurableSet, iUnion_setOf, measurableSet_comap]

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