rw [hX.map, PMF.map_toMeasure _ this, PMF.map_not_bernoulli']
α : 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 μ
a : α
this : Measurable Not
⊢ Measure.map Not (Measure.map (fun ω => a ∈ X ω) μ) = (PMF.bernoulli' (1 - p) ⋯).toMeasure
no goals