condIndepSets_piiUnionInter_of_disjoint

English

If iCondIndepSets m' hm' s μ holds and S, T are disjoint, then CondIndepSets m' hm' (πiUnionInter s S) (πiUnionInter s T) μ holds.

Русский

Если iCondIndepSets m' hm' s μ выполняется и S, T несовместны, тогда CondIndepSets между объединением по π и пересечением по π держится.

LaTeX

$$$\mathrm{CondIndepSets}(m', hm', (\pi i\!\!_{i} s_i), (\pi i\!\!_{i} s_i), \mu) \text{ with } S, T \text{ disjoint}$$$

Lean4

theorem condIndepSets_piiUnionInter_of_disjoint {s : ι → Set (Set Ω)} {S T : Set ι}
    (h_indep : iCondIndepSets m' hm' s μ) (hST : Disjoint S T) :
    CondIndepSets m' hm' (piiUnionInter s S) (piiUnionInter s T) μ :=
  Kernel.indepSets_piiUnionInter_of_disjoint h_indep hST

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