iCondIndepSet_iff — Mathlib

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]

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