condIndepSets — Mathlib

English

If CondIndep m' hm' p1 p2 μ holds for p1, p2 that are Pi-systems, then CondIndepSets m' hm' p1 p2 μ holds, and conversely CondIndepSets implies CondIndep.

Русский

Если CondIndep m' hm' p1 p2 μ справедлива для Pi-систем p1, p2, тогда CondIndepSets m' hm' p1 p2 μ, и наоборот.

LaTeX

$$$\mathrm{CondIndepSets}(m', hm', p_1, p_2, \mu) \iff \mathrm{CondIndep}(m', \operatorname{generateFrom}(p_1), \operatorname{generateFrom}(p_2), hm', \mu).$$$

Lean4

theorem condIndepSets {s1 s2 : Set (Set Ω)} (h_indep : CondIndep m' (generateFrom s1) (generateFrom s2) hm' μ) :
    CondIndepSets m' hm' s1 s2 μ :=
  Kernel.Indep.indepSets h_indep

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