indepSets_piiUnionInter_of_disjoint

English

If iIndepSets s μ holds, then independence persists across piiUnionInter of two disjoint index sets S and T.

Русский

Если iIndepSets s μ верно, то независимость сохраняется для piiUnionInter s S и piiUnionInter s T приDisjoint(S,T).

LaTeX

$$iIndepSets s μ → Disjoint S T → IndepSets (piiUnionInter s S) (piiUnionInter s T) μ$$

Lean4

theorem indepSets_piiUnionInter_of_disjoint {s : ι → Set (Set Ω)} {S T : Set ι} (h_indep : iIndepSets s μ)
    (hST : Disjoint S T) : IndepSets (piiUnionInter s S) (piiUnionInter s T) μ :=
  Kernel.indepSets_piiUnionInter_of_disjoint h_indep hST

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