equal
deleted
inserted
replaced
201 then guess A unfolding choice_iff .. note A = this |
201 then guess A unfolding choice_iff .. note A = this |
202 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 |
202 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 |
203 have A_notempty: "\<And>i. i \<in> domain x \<Longrightarrow> A i \<noteq> {}" using open_sub[of _ "\<lambda>_. UNIV"] by auto |
203 have A_notempty: "\<And>i. i \<in> domain x \<Longrightarrow> A i \<noteq> {}" using open_sub[of _ "\<lambda>_. UNIV"] by auto |
204 let ?A = "(\<lambda>f. Pi' (domain x) f) ` (Pi\<^sub>E (domain x) A)" |
204 let ?A = "(\<lambda>f. Pi' (domain x) f) ` (Pi\<^sub>E (domain x) A)" |
205 show "\<exists>A::nat \<Rightarrow> ('a\<Rightarrow>\<^sub>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))" |
205 show "\<exists>A::nat \<Rightarrow> ('a\<Rightarrow>\<^sub>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))" |
206 proof (rule first_countableI[where A="?A"], safe) |
206 proof (rule first_countableI[of "?A"], safe) |
207 show "countable ?A" using A by (simp add: countable_PiE) |
207 show "countable ?A" using A by (simp add: countable_PiE) |
208 next |
208 next |
209 fix S::"('a \<Rightarrow>\<^sub>F 'b) set" assume "open S" "x \<in> S" |
209 fix S::"('a \<Rightarrow>\<^sub>F 'b) set" assume "open S" "x \<in> S" |
210 thus "\<exists>a\<in>?A. a \<subseteq> S" unfolding open_fmap_def |
210 thus "\<exists>a\<in>?A. a \<subseteq> S" unfolding open_fmap_def |
211 proof (induct rule: generate_topology.induct) |
211 proof (induct rule: generate_topology.induct) |