iCondIndepSet_iff_iCondIndep — Mathlib

English

For a set s of subsets, iCondIndepSet m' hm' s μ is equivalent to iCondIndep m' hm' (generatedFrom {s i}) μ.

Русский

Для множества множеств s верно, что iCondIndepSet m' hm' s μ эквивалентно iCondIndep m' hm' (generateFrom {s_i}) μ.

LaTeX

$$$iCondIndepSet(m', hm', s, μ) \\iff iCondIndep(m', hm', (\\lambda i. \\text{generateFrom}({s_i})), μ)$$

Lean4

theorem iCondIndepSet_iff_iCondIndep (s : ι → Set Ω) (μ : Measure Ω) [IsFiniteMeasure μ] :
    iCondIndepSet m' hm' s μ ↔ iCondIndep m' hm' (fun i ↦ generateFrom {s i}) μ := by
  simp only [iCondIndepSet, iCondIndep, Kernel.iIndepSet]

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