src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
changeset 68120 2f161c6910f7
parent 68073 fad29d2a17a5
child 68239 0764ee22a4d1
     1.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun May 06 23:59:14 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue May 08 10:32:07 2018 +0100
     1.3 @@ -334,7 +334,7 @@
     1.4          \<exists>z. (?F has_integral z) (cbox a b) \<and> norm (z - k2) < norm (k1 - k2)/2"
     1.5      by (rule has_integral_altD[OF assms(2) nonbox,OF e]) blast
     1.6    obtain a b :: 'n where ab: "ball 0 B1 \<subseteq> cbox a b" "ball 0 B2 \<subseteq> cbox a b"
     1.7 -    by (metis Un_subset_iff bounded_Un bounded_ball bounded_subset_cbox)
     1.8 +    by (metis Un_subset_iff bounded_Un bounded_ball bounded_subset_cbox_symmetric)
     1.9    obtain w where w: "(?F has_integral w) (cbox a b)" "norm (w - k1) < norm (k1 - k2)/2"
    1.10      using B1(2)[OF ab(1)] by blast
    1.11    obtain z where z: "(?F has_integral z) (cbox a b)" "norm (z - k2) < norm (k1 - k2)/2"
    1.12 @@ -1635,9 +1635,9 @@
    1.13          using has_integral_altD[OF _ False ij] assms by blast
    1.14        have "bounded (ball 0 B1 \<union> ball (0::'a) B2)"
    1.15          unfolding bounded_Un by(rule conjI bounded_ball)+
    1.16 -      from bounded_subset_cbox[OF this] 
    1.17 +      from bounded_subset_cbox_symmetric[OF this] 
    1.18        obtain a b::'a where ab: "ball 0 B1 \<subseteq> cbox a b" "ball 0 B2 \<subseteq> cbox a b"
    1.19 -        by blast+
    1.20 +        by (meson Un_subset_iff)
    1.21        then obtain w1 w2 where int_w1: "((\<lambda>x. if x \<in> S then f x else 0) has_integral w1) (cbox a b)"
    1.22                          and norm_w1:  "norm (w1 - i) < (i \<bullet> k - j \<bullet> k) / 3"
    1.23                          and int_w2: "((\<lambda>x. if x \<in> S then g x else 0) has_integral w2) (cbox a b)"
    1.24 @@ -6227,7 +6227,7 @@
    1.25          \<exists>z. (?g has_integral z) (cbox a b) \<and> norm (z - integral S g) < e/2"
    1.26        using integrable_integral [OF int_g,unfolded has_integral'[of g]] e that by blast
    1.27      obtain a b::'n where ab: "ball 0 Bf \<union> ball 0 Bg \<subseteq> cbox a b"
    1.28 -      using ball_max_Un bounded_subset_cbox[OF bounded_ball, of _ "max Bf Bg"] by blast
    1.29 +      using ball_max_Un  by (metis bounded_ball bounded_subset_cbox_symmetric)
    1.30      have "ball 0 Bf \<subseteq> cbox a b"
    1.31        using ab by auto
    1.32      with Bf obtain z where int_fz: "(?f has_integral z) (cbox a b)" and z: "norm (z - integral S f) < e/2"