English
If iCondIndepSets m' hm' s μ holds and S, T are disjoint, then CondIndepSets m' hm' (piiUnionInter s S) (piiUnionInter s T) μ holds.
Русский
Если iCondIndepSets m' hm' s μ выполняется и S, T несовместны, то CondIndepSets между piiUnionInter s S и piiUnionInter s T держится.
LaTeX
$$$\mathrm{CondIndepSets}(m', hm', \mathrm{piiUnionInter}(s, S), \mathrm{piiUnionInter}(s, T), \mu).$$$
Lean4
/-- The σ-algebras generated by conditionally independent pi-systems are conditionally independent.
-/
theorem iCondIndep (m : ι → MeasurableSpace Ω) (h_le : ∀ i, m i ≤ mΩ) (π : ι → Set (Set Ω))
(h_pi : ∀ n, IsPiSystem (π n)) (h_generate : ∀ i, m i = generateFrom (π i)) (h_ind : iCondIndepSets m' hm' π μ) :
iCondIndep m' hm' m μ :=
Kernel.iIndepSets.iIndep m h_le π h_pi h_generate h_ind