equal
deleted
inserted
replaced
308 qed fact |
308 qed fact |
309 also have "\<dots> = (LINT x:(A - A \<inter> B)|M. f x) + (LINT x:(B - A \<inter> B)|M. f x)" |
309 also have "\<dots> = (LINT x:(A - A \<inter> B)|M. f x) + (LINT x:(B - A \<inter> B)|M. f x)" |
310 by (auto intro!: set_integral_Un set_integrable_subset[OF f]) |
310 by (auto intro!: set_integral_Un set_integrable_subset[OF f]) |
311 also have "\<dots> = (LINT x:A|M. f x) + (LINT x:B|M. f x)" |
311 also have "\<dots> = (LINT x:A|M. f x) + (LINT x:B|M. f x)" |
312 using ae |
312 using ae |
313 by (intro arg_cong2[where f="op+"] set_integral_cong_set) |
313 by (intro arg_cong2[where f="(+)"] set_integral_cong_set) |
314 (auto intro!: set_borel_measurable_subset[OF f']) |
314 (auto intro!: set_borel_measurable_subset[OF f']) |
315 finally show ?thesis . |
315 finally show ?thesis . |
316 qed |
316 qed |
317 |
317 |
318 lemma set_integral_finite_Union: |
318 lemma set_integral_finite_Union: |