indepSets — Mathlib

English

If IndepSets s κ μ holds for sigma-algebras s1 and s2, then the generated sigma-algebras preserve independence.

Русский

Если IndepSets выполняется для систем s1 и s2, то порожденные сигма-алгебры сохраняют независимость.

LaTeX

$$IndepSets s1 s2 κ μ → Indep s1 s2 κ μ$$

Lean4

theorem indepSets {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α} {s1 s2 : Set (Set Ω)}
    (h_indep : Indep (generateFrom s1) (generateFrom s2) κ μ) : IndepSets s1 s2 κ μ := fun t1 t2 ht1 ht2 =>
  h_indep t1 t2 (measurableSet_generateFrom ht1) (measurableSet_generateFrom ht2)

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