∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s₁ s₂ s' : Set (Set Ω)},
  ProbabilityTheory.IndepSets s₁ s' μ → ProbabilityTheory.IndepSets s₂ s' μ → ProbabilityTheory.IndepSets (s₁ ∪ s₂) s' μ