∀ {Ω : 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 μ ↔ ProbabilityTheory.iCondIndepSets m' hm' (fun i => {s i}) μ