equal
deleted
inserted
replaced
239 using finite_list by auto |
239 using finite_list by auto |
240 |
240 |
241 lemma countable_Collect_finite: "countable (Collect (finite::'a::countable set\<Rightarrow>bool))" |
241 lemma countable_Collect_finite: "countable (Collect (finite::'a::countable set\<Rightarrow>bool))" |
242 by (simp add: Collect_finite_eq_lists) |
242 by (simp add: Collect_finite_eq_lists) |
243 |
243 |
|
244 lemma countable_rat: "countable \<rat>" |
|
245 unfolding Rats_def by auto |
|
246 |
|
247 lemma Collect_finite_subset_eq_lists: "{A. finite A \<and> A \<subseteq> T} = set ` lists T" |
|
248 using finite_list by (auto simp: lists_eq_set) |
|
249 |
|
250 lemma countable_Collect_finite_subset: |
|
251 "countable T \<Longrightarrow> countable {A. finite A \<and> A \<subseteq> T}" |
|
252 unfolding Collect_finite_subset_eq_lists by auto |
|
253 |
244 subsection {* Misc lemmas *} |
254 subsection {* Misc lemmas *} |
245 |
255 |
246 lemma countable_all: |
256 lemma countable_all: |
247 assumes S: "countable S" |
257 assumes S: "countable S" |
248 shows "(\<forall>s\<in>S. P s) \<longleftrightarrow> (\<forall>n::nat. from_nat_into S n \<in> S \<longrightarrow> P (from_nat_into S n))" |
258 shows "(\<forall>s\<in>S. P s) \<longleftrightarrow> (\<forall>n::nat. from_nat_into S n \<in> S \<longrightarrow> P (from_nat_into S n))" |