--- 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:
--- 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