condIndepSet_iff_condIndep — Mathlib

English

Independence between CondIndepSet and generated sigma-algebras: condIndepSet_iff_condIndep relates a CondIndepSet to CondIndep with generated-from σ-algebras.

Русский

Независимость CondIndepSet и порождённых сигма-алгебр: condIndepSet_iff_condIndep устанавливает эквивалентность между CondIndepSet и CondIndep с сигма-алгебрами, порождёнными множествами.

LaTeX

$$$CondIndepSet(m', hm', s, t, μ) \\iff CondIndep(m', generateFrom\\{s\\}, generateFrom\\{t\\}, hm', μ)$$$

Lean4

theorem condIndepSet_iff_condIndep (s t : Set Ω) (μ : Measure Ω) [IsFiniteMeasure μ] :
    CondIndepSet m' hm' s t μ ↔ CondIndep m' (generateFrom { s }) (generateFrom { t }) hm' μ := by
  simp only [CondIndepSet, CondIndep, Kernel.IndepSet]

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