English
Equivalence for iCondIndepSet_iff_iCondIndepSets_singleton with the standard lemmata; iCondIndepSet ↔ iCondIndepSets with singleton generators.
Русский
Эквивалентность для iCondIndepSet_iff_iCondIndepSets_singleton с использованием стандартных лемм; iCondIndepSet ↔ iCondIndepSets с порождёнными сигма-алгебрами-одиночками.
LaTeX
$$$iCondIndepSet(m', hm', s, μ) \\iff iCondIndepSets(m', hm', (\\lambda i. {s_i}), μ)$$$
Lean4
theorem iCondIndepSet_iff (s : ι → Set Ω) (hs : ∀ i, MeasurableSet (s i)) (μ : Measure Ω) [IsFiniteMeasure μ] :
iCondIndepSet m' hm' s μ ↔ ∀ S : Finset ι, μ⟦⋂ i ∈ S, s i|m'⟧ =ᵐ[μ] ∏ i ∈ S, μ⟦s i|m'⟧ := by
rw [iCondIndepSet_iff_iCondIndepSets_singleton _ _ _ hs, iCondIndepSets_singleton_iff _ _ _ hs]