generateFrom_prod_eq — Mathlib

English

The product of generated σ-algebras equals the σ-algebra generated by rectangles when both generators are countably spanning.

Русский

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

LaTeX

$$$\\mathrm{Prod}.\\mathrm{instMeasurableSpace} = \\mathrm{generateFrom}(\\{A \\times B \mid A\\in C, B\\in D\\})$$$

Lean4

/-- The product of generated σ-algebras is the one generated by rectangles, if both generating sets
  are countably spanning. -/
theorem generateFrom_prod_eq {α β} {C : Set (Set α)} {D : Set (Set β)} (hC : IsCountablySpanning C)
    (hD : IsCountablySpanning D) :
    @Prod.instMeasurableSpace _ _ (generateFrom C) (generateFrom D) = generateFrom (image2 (· ×ˢ ·) C D) :=
  by
  apply le_antisymm
  · refine sup_le ?_ ?_ <;> rw [comap_generateFrom] <;> apply generateFrom_le <;> rintro _ ⟨s, hs, rfl⟩
    · rcases hD with ⟨t, h1t, h2t⟩
      rw [← prod_univ, ← h2t, prod_iUnion]
      apply MeasurableSet.iUnion
      intro n
      apply measurableSet_generateFrom
      exact ⟨s, hs, t n, h1t n, rfl⟩
    · rcases hC with ⟨t, h1t, h2t⟩
      rw [← univ_prod, ← h2t, iUnion_prod_const]
      apply MeasurableSet.iUnion
      rintro n
      apply measurableSet_generateFrom
      exact mem_image2_of_mem (h1t n) hs
  · apply generateFrom_le
    rintro _ ⟨s, hs, t, ht, rfl⟩
    dsimp only
    rw [prod_eq]
    apply (measurable_fst _).inter (measurable_snd _)
    · exact measurableSet_generateFrom hs
    · exact measurableSet_generateFrom ht

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