piiUnionInter_of_notMem — Mathlib

English

If for every i, CondIndep m' hm' m_i hm' μ holds and m is antitone, then CondIndep m' (iSup_i m_i) m₁ hm' μ.

Русский

Если для каждого i верна CondIndep m' hm' m_i hm' μ и m антитонична, то CondIndep m' (iSup_i m_i) m₁ hm' μ.

LaTeX

$$$\mathrm{CondIndep}(m', \bigvee_i m_i, m_1, hm', \mu)$$$

Lean4

theorem piiUnionInter_of_notMem {π : ι → Set (Set Ω)} {a : ι} {S : Finset ι} (hp_ind : iCondIndepSets m' hm' π μ)
    (haS : a ∉ S) : CondIndepSets m' hm' (piiUnionInter π S) (π a) μ :=
  Kernel.iIndepSets.piiUnionInter_of_notMem hp_ind haS

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