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