iCondIndepSet_iff_iCondIndepSets_singleton

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

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