English
Let μ be a finite measure on Ω, and m', m1, m2 be sigma-algebras with hm' ≤ mΩ. Then CondIndep m' m1 m2 hm' μ holds if and only if for every s and t with s measurable for m1 and t measurable for m2, CondIndepSet m' hm' s t μ holds.
Русский
Пусть μ — конечная мера на Ω, а m', m1, m2 — сигма‑алгебры с hm' ≤ mΩ. Тогда CondIndep m' m1 m2 hm' μ эквивалентно тому, что для любых s и t, измеримых по m1 и m2 соответственно, CondIndepSet m' hm' s t μ выполняется.
LaTeX
$$$\operatorname{CondIndep}(m', m_1, m_2; \mu) \iff \forall s,t\,\big( \operatorname{MeasurableSet}_{m_1}(s) \to \operatorname{MeasurableSet}_{m_2}(t) \to \operatorname{CondIndepSet}(m' hm' s t \mu) \big)$$$
Lean4
theorem condIndep_iff_forall_condIndepSet (μ : Measure Ω) [IsFiniteMeasure μ] :
CondIndep m' m₁ m₂ hm' μ ↔ ∀ s t, MeasurableSet[m₁] s → MeasurableSet[m₂] t → CondIndepSet m' hm' s t μ :=
Kernel.indep_iff_forall_indepSet m₁ m₂ _ _
