equal
deleted
inserted
replaced
934 apply (auto intro!: positive_integral_cong arg_cong2[where f=emeasure] simp: space_pair_measure) |
934 apply (auto intro!: positive_integral_cong arg_cong2[where f=emeasure] simp: space_pair_measure) |
935 done |
935 done |
936 |
936 |
937 show ?B |
937 show ?B |
938 using IJ.measurable_emeasure_Pair1[OF merge] |
938 using IJ.measurable_emeasure_Pair1[OF merge] |
939 by (simp add: vimage_compose[symmetric] comp_def space_pair_measure cong: measurable_cong) |
939 by (simp add: vimage_comp comp_def space_pair_measure cong: measurable_cong) |
940 qed |
940 qed |
941 |
941 |
942 lemma (in product_sigma_finite) product_integral_insert: |
942 lemma (in product_sigma_finite) product_integral_insert: |
943 assumes I: "finite I" "i \<notin> I" |
943 assumes I: "finite I" "i \<notin> I" |
944 and f: "integrable (Pi\<^sub>M (insert i I) M) f" |
944 and f: "integrable (Pi\<^sub>M (insert i I) M) f" |