English
Independence with singleton generators: iCondIndepSet_iff_iCondIndepSets_singleton asserts equivalence between independence of sets and independence of the corresponding singleton-generated σ-algebras.
Русский
Независимость с генераторами-одиночками: tвердение эквивалентности между независимостью множеств и независимостью соответствующих сигма-алгебр, порождённых одиночками.
LaTeX
$$$iCondIndepSet(m', hm', s, μ) \\iff iCondIndepSets(m', hm', (\\lambda i. {s_i}), μ)$$$
Lean4
theorem iCondIndepSet_iff_iCondIndepSets_singleton (s : ι → Set Ω) (hs : ∀ i, MeasurableSet (s i)) (μ : Measure Ω)
[IsFiniteMeasure μ] : iCondIndepSet m' hm' s μ ↔ iCondIndepSets m' hm' (fun i ↦ {s i}) μ :=
Kernel.iIndepSet_iff_iIndepSets_singleton hs