equal
deleted
inserted
replaced
614 by (simp add: case_prod_app prod.case_distrib sum_distrib_left) |
614 by (simp add: case_prod_app prod.case_distrib sum_distrib_left) |
615 also have "\<dots> = e * (?\<mu> (\<Union>(x,r)\<in>I. ball x r) / ?\<mu> (ball z 1))" |
615 also have "\<dots> = e * (?\<mu> (\<Union>(x,r)\<in>I. ball x r) / ?\<mu> (ball z 1))" |
616 apply (subst measure_UNION') |
616 apply (subst measure_UNION') |
617 using that pwC by (auto simp: case_prod_unfold elim: pairwise_mono) |
617 using that pwC by (auto simp: case_prod_unfold elim: pairwise_mono) |
618 also have "\<dots> \<le> e" |
618 also have "\<dots> \<le> e" |
619 by (metis mult.commute mult.left_neutral mult_le_cancel_iff1 \<open>e > 0\<close> le1) |
619 by (metis mult.commute mult.left_neutral mult_le_cancel_right_pos \<open>e > 0\<close> le1) |
620 finally show ?thesis . |
620 finally show ?thesis . |
621 qed |
621 qed |
622 have "\<Union>(U ` C) \<in> lmeasurable" "?\<mu> (\<Union>(U ` C)) \<le> e" |
622 have "\<Union>(U ` C) \<in> lmeasurable" "?\<mu> (\<Union>(U ` C)) \<le> e" |
623 using \<open>e > 0\<close> Um lee |
623 using \<open>e > 0\<close> Um lee |
624 by(auto intro!: fmeasurable_UN_bound [OF \<open>countable C\<close>] measure_UN_bound [OF \<open>countable C\<close>]) |
624 by(auto intro!: fmeasurable_UN_bound [OF \<open>countable C\<close>] measure_UN_bound [OF \<open>countable C\<close>]) |