rwa [IndepFun_iff, MeasurableSpace.comap_compl measurable_compl,
  MeasurableSpace.comap_compl measurable_compl, ← IndepFun_iff]
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
⊢ IndepFun (fun ω => (X ω)ᶜ) (fun ω => (Y ω)ᶜ) μ
no goals