have : Measurable Not := fun _ _ ↦ trivial
α : 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 : α
⊢ Measure.map (fun ω => a ∈ (X ω)ᶜ) μ = (PMF.bernoulli' (1 - p) ⋯).toMeasure
α : 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 (fun ω => a ∈ (X ω)ᶜ) μ = (PMF.bernoulli' (1 - p) ⋯).toMeasure