src/HOL/Analysis/Vitali_Covering_Theorem.thy
 changeset 69313 b021008c5397 parent 68833 fde093888c16 child 69683 8b3458ca0762
```     1.1 --- a/src/HOL/Analysis/Vitali_Covering_Theorem.thy	Sun Nov 18 09:51:41 2018 +0100
1.2 +++ b/src/HOL/Analysis/Vitali_Covering_Theorem.thy	Sun Nov 18 18:07:51 2018 +0000
1.3 @@ -617,13 +617,13 @@
1.4                by (metis mult.commute mult.left_neutral real_mult_le_cancel_iff1 \<open>e > 0\<close> le1)
1.5              finally show ?thesis .
1.6            qed
1.7 -          have "UNION C U \<in> lmeasurable" "?\<mu> (\<Union>(U ` C)) \<le> e"
1.8 +          have "\<Union>(U ` C) \<in> lmeasurable" "?\<mu> (\<Union>(U ` C)) \<le> e"
1.9              using \<open>e > 0\<close> Um lee
1.10              by(auto intro!: fmeasurable_UN_bound [OF \<open>countable C\<close>] measure_UN_bound [OF \<open>countable C\<close>])
1.11          }
1.12 -        moreover have "?\<mu> ?T = ?\<mu> (UNION C U)"
1.13 -        proof (rule measure_negligible_symdiff [OF \<open>UNION C U \<in> lmeasurable\<close>])
1.14 -          show "negligible((UNION C U - ?T) \<union> (?T - UNION C U))"
1.15 +        moreover have "?\<mu> ?T = ?\<mu> (\<Union>(U ` C))"
1.16 +        proof (rule measure_negligible_symdiff [OF \<open>\<Union>(U ` C) \<in> lmeasurable\<close>])
1.17 +          show "negligible((\<Union>(U ` C) - ?T) \<union> (?T - \<Union>(U ` C)))"
1.18              by (force intro!: negligible_subset [OF negC])
1.19          qed
1.20          ultimately show "?T \<in> lmeasurable"  "?\<mu> ?T \<le> e"
```