src/HOL/Library/Countable.thy
changeset 39198 f967a16dfcdd
parent 37715 44b27ea94a16
child 39250 548a3e5521ab
equal deleted inserted replaced
39166:19efc2af3e6c 39198:f967a16dfcdd
   137   obtain xs :: "'a list" where xs: "set xs = UNIV"
   137   obtain xs :: "'a list" where xs: "set xs = UNIV"
   138     using finite_list [OF finite_UNIV] ..
   138     using finite_list [OF finite_UNIV] ..
   139   show "\<exists>to_nat::('a \<Rightarrow> 'b) \<Rightarrow> nat. inj to_nat"
   139   show "\<exists>to_nat::('a \<Rightarrow> 'b) \<Rightarrow> nat. inj to_nat"
   140   proof
   140   proof
   141     show "inj (\<lambda>f. to_nat (map f xs))"
   141     show "inj (\<lambda>f. to_nat (map f xs))"
   142       by (rule injI, simp add: xs expand_fun_eq)
   142       by (rule injI, simp add: xs ext_iff)
   143   qed
   143   qed
   144 qed
   144 qed
   145 
   145 
   146 
   146 
   147 subsection {* The Rationals are Countably Infinite *}
   147 subsection {* The Rationals are Countably Infinite *}