[STATEMENT]
lemma nn_integral_measure_spmf':
  "(\<integral>\<^sup>+ x. f x \<partial>measure_spmf p) = \<integral>\<^sup>+ x. ennreal (spmf p x) * f x \<partial>count_space (set_spmf p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral\<^sup>N (measure_spmf p) f = \<integral>\<^sup>+ x. ennreal (spmf p x) * f x \<partial>count_space (set_spmf p)
[PROOF STEP]
by(auto simp add: nn_integral_measure_spmf nn_integral_count_space_indicator in_set_spmf_iff_spmf intro!: nn_integral_cong split: split_indicator)