∀ {Ω : Type u_1} {ι : Type u_2} {x : MeasurableSpace Ω} (π : ι → Set (Set Ω)) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.iIndepSets π μ ↔
    ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, f i ∈ π i) → μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)