src/HOL/Analysis/Set_Integral.thy
 changeset 69313 b021008c5397 parent 69173 38beaaebe736 child 69566 c41954ee87cf
```     1.1 --- a/src/HOL/Analysis/Set_Integral.thy	Sun Nov 18 09:51:41 2018 +0100
1.2 +++ b/src/HOL/Analysis/Set_Integral.thy	Sun Nov 18 18:07:51 2018 +0000
1.3 @@ -368,7 +368,7 @@
1.4    using assms
1.5  proof%unimportant induction
1.6    case (insert x F)
1.7 -  then have "A x \<inter> UNION F A = {}"
1.8 +  then have "A x \<inter> \<Union>(A ` F) = {}"
1.9      by (meson disjoint_family_on_insert)
1.10    with insert show ?case
1.11      by (simp add: set_integral_Un set_integrable_Un set_integrable_UN disjoint_family_on_insert)
1.12 @@ -453,7 +453,7 @@
1.13        set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))"
1.14        by simp
1.15    qed
1.16 -  show "LINT x|M. indicator (UNION UNIV A) x *\<^sub>R f x = LINT x|M. (\<Sum>i. indicator (A i) x *\<^sub>R f x)"
1.17 +  show "LINT x|M. indicator (\<Union>(A ` UNIV)) x *\<^sub>R f x = LINT x|M. (\<Sum>i. indicator (A i) x *\<^sub>R f x)"
1.18      apply (rule Bochner_Integration.integral_cong[OF refl])
1.19      apply (subst suminf_scaleR_left[OF sums_summable[OF indicator_sums, OF disj], symmetric])
1.20      using sums_unique[OF indicator_sums[OF disj]]
1.21 @@ -472,7 +472,7 @@
1.22      using intgbl by (rule set_integrable_subset) auto
1.23    show "\<And>i. (\<lambda>x. indicator (A i) x *\<^sub>R f x) \<in> borel_measurable M"
1.24      using int_A integrable_iff_bounded set_integrable_def by blast
1.25 -  show "(\<lambda>x. indicator (UNION UNIV A) x *\<^sub>R f x) \<in> borel_measurable M"
1.26 +  show "(\<lambda>x. indicator (\<Union>(A ` UNIV)) x *\<^sub>R f x) \<in> borel_measurable M"
1.27      using integrable_iff_bounded intgbl set_integrable_def by blast
1.28    show "integrable M (\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R norm (f x))"
1.29      using int_A intgbl integrable_norm unfolding set_integrable_def
1.30 @@ -501,7 +501,7 @@
1.31      by force
1.32    have "set_integrable M (\<Inter>i. A i) f"
1.33      using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
1.34 -  with int_A show "(\<lambda>x. indicat_real (INTER UNIV A) x *\<^sub>R f x) \<in> borel_measurable M"
1.35 +  with int_A show "(\<lambda>x. indicat_real (\<Inter>(A ` UNIV)) x *\<^sub>R f x) \<in> borel_measurable M"
1.36                    "\<And>i. (\<lambda>x. indicat_real (A i) x *\<^sub>R f x) \<in> borel_measurable M"
1.37      by (auto simp: set_integrable_def)
1.38    show "\<And>i. AE x in M. norm (indicator (A i) x *\<^sub>R f x) \<le> indicator (A 0) x *\<^sub>R norm (f x)"
```