# HG changeset patch
# User hoelzl
# Date 1358420352 -3600
# Node ID b28f258ebc1aecd83e9b84aa64e8110db8f09992
# Parent  cfdf19d3ca326501b32761bbe17468d6c334113f
countablility of finite subsets and rational numbers

diff -r cfdf19d3ca32 -r b28f258ebc1a src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Thu Jan 17 11:57:17 2013 +0100
+++ b/src/HOL/Library/Countable_Set.thy	Thu Jan 17 11:59:12 2013 +0100
@@ -241,6 +241,16 @@
 lemma countable_Collect_finite: "countable (Collect (finite::'a::countable set\<Rightarrow>bool))"
   by (simp add: Collect_finite_eq_lists)
 
+lemma countable_rat: "countable \<rat>"
+  unfolding Rats_def by auto
+
+lemma Collect_finite_subset_eq_lists: "{A. finite A \<and> A \<subseteq> T} = set ` lists T"
+  using finite_list by (auto simp: lists_eq_set)
+
+lemma countable_Collect_finite_subset:
+  "countable T \<Longrightarrow> countable {A. finite A \<and> A \<subseteq> T}"
+  unfolding Collect_finite_subset_eq_lists by auto
+
 subsection {* Misc lemmas *}
 
 lemma countable_all:
diff -r cfdf19d3ca32 -r b28f258ebc1a src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 11:57:17 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 11:59:12 2013 +0100
@@ -21,9 +21,6 @@
   "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)"
   by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq)
 
-lemma countable_rat: "countable \<rat>"
-  unfolding Rats_def by auto
-
 subsection {* Topological Basis *}
 
 context topological_space