rw [← hX.map a, h, Measure.map_zero]
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : Nonempty α
a : α
h : μ = 0
⊢ (PMF.bernoulli' p ⋯).toMeasure = 0
no goals