∀ {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  (hm' : m' ≤ mΩ) (s : ι → Set Ω),
  (∀ (i : ι), MeasurableSet (s i)) →
    ∀ (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
      ProbabilityTheory.iCondIndepSet m' hm' s μ ↔
        ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω => 1 | m'] =ᵐ[μ] ∏ i ∈ S, μ[(s i).indicator fun ω => 1 | m']