Theorem: PMF.map_toMeasure (LeanCamCombi/Mathlib/Probability/ProbabilityMassFunction/Constructions.lean)

State before:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p : PMF α
hf : Measurable f
⊢ Measure.map f p.toMeasure = (map f p).toMeasure
Tactic:
ext s hs : 1
State after:
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p : PMF α
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (Measure.map f p.toMeasure) s = (map f p).toMeasure s

State before:
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p : PMF α
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (Measure.map f p.toMeasure) s = (map f p).toMeasure s
Tactic:
rw [PMF.toMeasure_map_apply _ _ _ hf hs, Measure.map_apply hf hs]
State after:
no goals