English
Let Ω carry a finite measure μ and m', m1, m2 be sigma-algebras on Ω with m' ≤ mΩ. If X and Y are conditionally independent given m' with respect to μ, then for every set s that is measurable with respect to m1 and every set t that is measurable with respect to m2, the pair (s, t) is conditionally independent given m'.
Русский
Пусть Ω оснащено конечной мерой μ, а m', m1, m2 — сигма‑алгебры на Ω с hm' : m' ≤ mΩ. Если X и Y условно независимы относительно m' по отношению к μ, тогда для любых s измеримого по m1 и t измеримого по m2 выполняется условная независимость s и t относительно m'.
LaTeX
$$$\operatorname{CondIndep}(m', m_1, m_2; \mu) \Rightarrow \forall s,t\big( \operatorname{MeasurableSet}_{m_1}(s) \land \operatorname{MeasurableSet}_{m_2}(t) \Rightarrow \operatorname{CondIndepSet}(m' hm' s t \mu) \big)$$$
Lean4
theorem condIndepSet_of_measurableSet {μ : Measure Ω} [IsFiniteMeasure μ] (h_indep : CondIndep m' m₁ m₂ hm' μ)
{s t : Set Ω} (hs : MeasurableSet[m₁] s) (ht : MeasurableSet[m₂] t) : CondIndepSet m' hm' s t μ :=
Kernel.Indep.indepSet_of_measurableSet h_indep hs ht
