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)"