src/HOL/Probability/Regularity.thy
changeset 58184 db1381d811ab
parent 56544 b60d5d119489
child 58876 1888e3cb8048
     1.1 --- a/src/HOL/Probability/Regularity.thy	Thu Sep 04 11:53:39 2014 +0200
     1.2 +++ b/src/HOL/Probability/Regularity.thy	Thu Sep 04 14:02:37 2014 +0200
     1.3 @@ -163,7 +163,7 @@
     1.4      by blast
     1.5    then obtain k where k: "\<forall>e\<in>{0<..}. \<forall>n\<in>{0<..}. measure M (space M) - e * 2 powr - real (n::nat)
     1.6      \<le> measure M (\<Union>i\<in>{0..k e n}. cball (from_nat_into X i) (1 / n))"
     1.7 -    apply atomize_elim unfolding bchoice_iff .
     1.8 +    by metis
     1.9    hence k: "\<And>e n. e > 0 \<Longrightarrow> n > 0 \<Longrightarrow> measure M (space M) - e * 2 powr - n
    1.10      \<le> measure M (\<Union>i\<in>{0..k e n}. cball (from_nat_into X i) (1 / n))"
    1.11      unfolding Ball_def by blast
    1.12 @@ -209,8 +209,8 @@
    1.13        from nat_approx_posE[OF this] guess n . note n = this
    1.14        let ?k = "from_nat_into X ` {0..k e (Suc n)}"
    1.15        have "finite ?k" by simp
    1.16 -      moreover have "K \<subseteq> \<Union>((\<lambda>x. ball x e') ` ?k)" unfolding K_def B_def using n by force
    1.17 -      ultimately show "\<exists>k. finite k \<and> K \<subseteq> \<Union>((\<lambda>x. ball x e') ` k)" by blast
    1.18 +      moreover have "K \<subseteq> (\<Union>x\<in>?k. ball x e')" unfolding K_def B_def using n by force
    1.19 +      ultimately show "\<exists>k. finite k \<and> K \<subseteq> (\<Union>x\<in>k. ball x e')" by blast
    1.20      qed
    1.21      ultimately
    1.22      show "?thesis e " by (auto simp: sU)