α : Type u_1
β : Type ?u.141584
γ : Type ?u.141587
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
s : Set α
hs : MeasurableSet s
⊢ (∑' (x : α), Set.indicator s (↑(toPmf μ)) x) = ∑' (x : α), Set.indicator s (fun x => ↑↑μ {x}) x
α : Type u_1
β : Type ?u.141584
γ : Type ?u.141587
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
s : Set α
hs : MeasurableSet s
⊢ ↑↑(toMeasure (toPmf μ)) s = ↑↑μ s
rw [μ.toPmf.toMeasure_apply s hs, ← μ.tsum_indicator_apply_singleton s hs]
no goals
α : Type u_1
β : Type ?u.141584
γ : Type ?u.141587
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
s : Set α
hs : MeasurableSet s
⊢ (∑' (x : α), Set.indicator s (↑(toPmf μ)) x) = ∑' (x : α), Set.indicator s (fun x => ↑↑μ {x}) x
rfl