∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {s₁ s₂ s₃ : Set (Set Ω)} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α},
  ProbabilityTheory.Kernel.IndepSets s₁ s₂ κ μ → s₃ ⊆ s₁ → ProbabilityTheory.Kernel.IndepSets s₃ s₂ κ μ