English
If each m_i is a sub-sigma-algebra generated by a pi-system π_i and these pi-systems are independent with respect to μ, then the family of generated sigma-algebras m_i is independent with respect to μ.
Русский
Если каждая m_i является подσ-алгеброй, порожденной π-системой π_i, и эти π-системы независимы по отношению к μ, то множество порожденных σ-алгебр m_i независимо по μ.
LaTeX
$$$\Big(\forall i, m_i = \mathrm{generateFrom}(π_i)\Big) \land (\forall n, IsPiSystem(π_n)) \Rightarrow iIndepSets(π, μ) \Rightarrow iIndep(m, μ)$$$
Lean4
/-- The measurable space structures generated by independent pi-systems are independent. -/
theorem iIndep (h_le : ∀ i, m i ≤ _mΩ) (π : ι → Set (Set Ω)) (h_pi : ∀ n, IsPiSystem (π n))
(h_generate : ∀ i, m i = generateFrom (π i)) (h_ind : iIndepSets π μ) : iIndep m μ :=
Kernel.iIndepSets.iIndep m h_le π h_pi h_generate h_ind
