src/HOL/Library/Countable_Set.thy
changeset 50936 b28f258ebc1a
parent 50245 dea9363887a6
child 51542 738598beeb26
     1.1 --- a/src/HOL/Library/Countable_Set.thy	Thu Jan 17 11:57:17 2013 +0100
     1.2 +++ b/src/HOL/Library/Countable_Set.thy	Thu Jan 17 11:59:12 2013 +0100
     1.3 @@ -241,6 +241,16 @@
     1.4  lemma countable_Collect_finite: "countable (Collect (finite::'a::countable set\<Rightarrow>bool))"
     1.5    by (simp add: Collect_finite_eq_lists)
     1.6  
     1.7 +lemma countable_rat: "countable \<rat>"
     1.8 +  unfolding Rats_def by auto
     1.9 +
    1.10 +lemma Collect_finite_subset_eq_lists: "{A. finite A \<and> A \<subseteq> T} = set ` lists T"
    1.11 +  using finite_list by (auto simp: lists_eq_set)
    1.12 +
    1.13 +lemma countable_Collect_finite_subset:
    1.14 +  "countable T \<Longrightarrow> countable {A. finite A \<and> A \<subseteq> T}"
    1.15 +  unfolding Collect_finite_subset_eq_lists by auto
    1.16 +
    1.17  subsection {* Misc lemmas *}
    1.18  
    1.19  lemma countable_all: