equal
deleted
inserted
replaced
646 qed |
646 qed |
647 also have "\<dots> = (\<Sum>y\<in>f`space M. (\<Sum>z\<in>g`space M. |
647 also have "\<dots> = (\<Sum>y\<in>f`space M. (\<Sum>z\<in>g`space M. |
648 if \<exists>x\<in>space M. y = f x \<and> z = g x then y * emeasure M {x\<in>space M. g x = z} else 0))" |
648 if \<exists>x\<in>space M. y = f x \<and> z = g x then y * emeasure M {x\<in>space M. g x = z} else 0))" |
649 by (auto intro!: sum.cong simp: sum_distrib_left) |
649 by (auto intro!: sum.cong simp: sum_distrib_left) |
650 also have "\<dots> = ?r" |
650 also have "\<dots> = ?r" |
651 by (subst sum.commute) |
651 by (subst sum.swap) |
652 (auto intro!: sum.cong simp: sum.If_cases scaleR_sum_right[symmetric] eq) |
652 (auto intro!: sum.cong simp: sum.If_cases scaleR_sum_right[symmetric] eq) |
653 finally show "integral\<^sup>S M f = ?r" . |
653 finally show "integral\<^sup>S M f = ?r" . |
654 qed |
654 qed |
655 |
655 |
656 lemma simple_integral_add[simp]: |
656 lemma simple_integral_add[simp]: |