src/HOL/Library/Countable_Set.thy
changeset 50245 dea9363887a6
parent 50148 b8cff6a8fda2
child 50936 b28f258ebc1a
     1.1 --- a/src/HOL/Library/Countable_Set.thy	Tue Nov 27 11:29:47 2012 +0100
     1.2 +++ b/src/HOL/Library/Countable_Set.thy	Tue Nov 27 13:48:40 2012 +0100
     1.3 @@ -235,6 +235,12 @@
     1.4      by (auto dest: subset_range_from_nat_into countable_subset lists_mono)
     1.5  qed
     1.6  
     1.7 +lemma Collect_finite_eq_lists: "Collect finite = set ` lists UNIV"
     1.8 +  using finite_list by auto
     1.9 +
    1.10 +lemma countable_Collect_finite: "countable (Collect (finite::'a::countable set\<Rightarrow>bool))"
    1.11 +  by (simp add: Collect_finite_eq_lists)
    1.12 +
    1.13  subsection {* Misc lemmas *}
    1.14  
    1.15  lemma countable_all: