src/HOL/Probability/Fin_Map.thy
changeset 51473 1210309fddab
parent 51343 b61b32f62c78
child 51489 f738e6dbd844
     1.1 --- a/src/HOL/Probability/Fin_Map.thy	Fri Mar 22 10:41:43 2013 +0100
     1.2 +++ b/src/HOL/Probability/Fin_Map.thy	Fri Mar 22 10:41:43 2013 +0100
     1.3 @@ -222,8 +222,8 @@
     1.4    hence open_sub: "\<And>i S. i\<in>domain x \<Longrightarrow> open (S i) \<Longrightarrow> x i\<in>(S i) \<Longrightarrow> (\<exists>a\<in>A i. a\<subseteq>(S i))" by auto
     1.5    have A_notempty: "\<And>i. i \<in> domain x \<Longrightarrow> A i \<noteq> {}" using open_sub[of _ "\<lambda>_. UNIV"] by auto
     1.6    let ?A = "(\<lambda>f. Pi' (domain x) f) ` (Pi\<^isub>E (domain x) A)"
     1.7 -  show "\<exists>A. countable A \<and> (\<forall>a\<in>A. x \<in> a \<and> open a) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S))"
     1.8 -  proof (rule exI[where x="?A"], safe)
     1.9 +  show "\<exists>A::nat \<Rightarrow> ('a\<Rightarrow>\<^isub>F'b) set. (\<forall>i. x \<in> (A i) \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))"
    1.10 +  proof (rule first_countableI[where A="?A"], safe)
    1.11      show "countable ?A" using A by (simp add: countable_PiE)
    1.12    next
    1.13      fix S::"('a \<Rightarrow>\<^isub>F 'b) set" assume "open S" "x \<in> S"