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"