src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
changeset 69313 b021008c5397
parent 69064 5840724b1d71
child 69508 2a4c8a2a3f8e
     1.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Nov 18 09:51:41 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Nov 18 18:07:51 2018 +0000
     1.3 @@ -5635,15 +5635,15 @@
     1.4          using qq by auto
     1.5        show "\<And>i1 i2. \<lbrakk>i1 \<in> r; i2 \<in> r; i1 \<noteq> i2\<rbrakk> \<Longrightarrow> interior i1 \<inter> interior i2 = {}"
     1.6          by (simp add: q'(5) r_def)
     1.7 -      show "interior (UNION p snd) \<inter> interior (\<Union>r) = {}"
     1.8 +      show "interior (\<Union>(snd ` p)) \<inter> interior (\<Union>r) = {}"
     1.9        proof (rule Int_interior_Union_intervals [OF \<open>finite r\<close>])
    1.10 -        show "open (interior (UNION p snd))"
    1.11 +        show "open (interior (\<Union>(snd ` p)))"
    1.12            by blast
    1.13          show "\<And>T. T \<in> r \<Longrightarrow> \<exists>a b. T = cbox a b"
    1.14            by (simp add: q'(4) r_def)
    1.15          have "finite (snd ` p)"
    1.16            by (simp add: p'(1))
    1.17 -        then show "\<And>T. T \<in> r \<Longrightarrow> interior (UNION p snd) \<inter> interior T = {}"
    1.18 +        then show "\<And>T. T \<in> r \<Longrightarrow> interior (\<Union>(snd ` p)) \<inter> interior T = {}"
    1.19            apply (subst Int_commute)
    1.20            apply (rule Int_interior_Union_intervals)
    1.21            using r_def q'(5) q(1) apply auto
    1.22 @@ -5672,7 +5672,7 @@
    1.23        then show "content L *\<^sub>R f x = 0"
    1.24          unfolding uv content_eq_0_interior[symmetric] by auto
    1.25      qed
    1.26 -    show "finite (UNION r qq)"
    1.27 +    show "finite (\<Union>(qq ` r))"
    1.28        by (meson finite_UN qq \<open>finite r\<close> tagged_division_of_finite)
    1.29    qed
    1.30    moreover have "content M *\<^sub>R f x = 0"