∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {s t : Set Ω},
  MeasurableSet s →
    MeasurableSet t →
      ∀ (μ : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.indepSet_iff_indepSets_singleton._auto_1)
        [MeasureTheory.IsZeroOrProbabilityMeasure μ],
        ProbabilityTheory.IndepSet s t μ ↔ ProbabilityTheory.IndepSets {s} {t} μ