src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
changeset 68120 2f161c6910f7
parent 68073 fad29d2a17a5
child 68403 223172b97d0b
     1.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun May 06 23:59:14 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Tue May 08 10:32:07 2018 +0100
     1.3 @@ -1978,7 +1978,7 @@
     1.4    and   measure_countable_negligible_Union_bounded:    "(\<lambda>n. (measure lebesgue (S n))) sums measure lebesgue (\<Union>n. S n)" (is ?Sums)
     1.5  proof -
     1.6    obtain a b where ab: "(\<Union>n. S n) \<subseteq> cbox a b"
     1.7 -    using bo bounded_subset_cbox by blast
     1.8 +    using bo bounded_subset_cbox_symmetric by metis
     1.9    then have B: "(\<Sum>k\<le>n. measure lebesgue (S k)) \<le> measure lebesgue (cbox a b)" for n
    1.10    proof -
    1.11      have "(\<Sum>k\<le>n. measure lebesgue (S k)) = measure lebesgue (UNION {..n} S)"
    1.12 @@ -2837,7 +2837,7 @@
    1.13        if "bounded S" "S \<in> lmeasurable" for S
    1.14      proof -
    1.15        obtain a b where "S \<subseteq> cbox a b"
    1.16 -        using \<open>bounded S\<close> bounded_subset_cbox by blast
    1.17 +        using \<open>bounded S\<close> bounded_subset_cbox_symmetric by metis
    1.18        have fUD: "(f ` \<Union>\<D>) \<in> lmeasurable \<and> ?\<mu> (f ` \<Union>\<D>) = (m * ?\<mu> (\<Union>\<D>))"
    1.19          if "countable \<D>"
    1.20            and cbox: "\<And>K. K \<in> \<D> \<Longrightarrow> K \<subseteq> cbox a b \<and> K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
    1.21 @@ -3005,7 +3005,7 @@
    1.22          "\<And>a b. ball 0 B \<subseteq> cbox a b \<Longrightarrow> \<bar>?\<mu> (S \<inter> cbox a b) - ?\<mu> S\<bar> < e / (1 + \<bar>m\<bar>)"
    1.23          using has_measure_limit [OF S] \<open>e > 0\<close> by (metis abs_add_one_gt_zero zero_less_divide_iff)
    1.24        obtain c d::'n where cd: "ball 0 B \<subseteq> cbox c d"
    1.25 -        using bounded_subset_cbox by blast
    1.26 +        by (metis bounded_subset_cbox_symmetric bounded_ball)
    1.27        with B have less: "\<bar>?\<mu> (S \<inter> cbox c d) - ?\<mu> S\<bar> < e / (1 + \<bar>m\<bar>)" .
    1.28        obtain D where "D > 0" and D: "cbox c d \<subseteq> ball 0 D"
    1.29          by (metis bounded_cbox bounded_subset_ballD)