generateFrom_pi_eq — Mathlib

English

If each C_i is countably spanning, then the product of generated spaces equals the generated space from boxes.

Русский

Если каждый C_i является счетно покрывающей, то произведение сгенерированных σ-алгебр равно σ-алгебре, генерируемой коробками.

LaTeX

$$$\\forall i, IsCountablySpanning(C_i) \\Rightarrow \\mathrm{generateFrom}(\\pi univ '' \\pi univ C) = \\mathrm{pi}$$$

Lean4

/-- The product of generated σ-algebras is the one generated by boxes, if both generating sets
  are countably spanning. -/
theorem generateFrom_pi_eq {C : ∀ i, Set (Set (α i))} (hC : ∀ i, IsCountablySpanning (C i)) :
    (@MeasurableSpace.pi _ _ fun i => generateFrom (C i)) = generateFrom (pi univ '' pi univ C) := by
  classical
  cases nonempty_encodable ι
  apply le_antisymm
  · refine iSup_le ?_; intro i; rw [comap_generateFrom]
    apply generateFrom_le; rintro _ ⟨s, hs, rfl⟩
    choose t h1t h2t using hC
    simp_rw [eval_preimage, ← h2t]
    rw [← @iUnion_const _ ℕ _ s]
    have :
      Set.pi univ (update (fun i' : ι => iUnion (t i')) i (⋃ _ : ℕ, s)) =
        Set.pi univ fun k => ⋃ j : ℕ, @update ι (fun i' => Set (α i')) _ (fun i' => t i' j) i s k :=
      by
      ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
      by_cases h : i' = i
      · subst h; simp
      · simp [h]
    rw [this, ← iUnion_univ_pi]
    apply MeasurableSet.iUnion
    intro n; apply measurableSet_generateFrom
    apply mem_image_of_mem; intro j _; dsimp only
    by_cases h : j = i
    · subst h; rwa [update_self]
    · rw [update_of_ne h]; apply h1t
  · apply generateFrom_le; rintro _ ⟨s, hs, rfl⟩
    rw [univ_pi_eq_iInter]; apply MeasurableSet.iInter; intro i
    apply @measurable_pi_apply _ _ (fun i => generateFrom (C i))
    exact measurableSet_generateFrom (hs i (mem_univ i))

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