src/HOL/Library/Countable_Set.thy

     show False
       by auto
   qed
 qed
 
+lemma transfer_countable[transfer_rule]:
+  "bi_unique R \<Longrightarrow> rel_fun (rel_set R) op = countable countable"
+  by (rule rel_funI, erule (1) bi_unique_rel_set_lemma)
+     (auto dest: countable_image_inj_on)
+
 subsection \<open>Uncountable\<close>
 
 abbreviation uncountable where
   "uncountable A \<equiv> \<not> countable A"
 

   by (auto intro: inj_on_inv_into simp: countable_def)
      (metis all_not_in_conv inj_on_iff_surj subset_UNIV)
 
 lemma uncountable_bij_betw: "bij_betw f A B \<Longrightarrow> uncountable B \<Longrightarrow> uncountable A"
   unfolding bij_betw_def by (metis countable_image)
-  
+
 lemma uncountable_infinite: "uncountable A \<Longrightarrow> infinite A"
   by (metis countable_finite)
-  
+
 lemma uncountable_minus_countable:
   "uncountable A \<Longrightarrow> countable B \<Longrightarrow> uncountable (A - B)"
   using countable_Un[of B "A - B"] assms by auto
 
 lemma countable_Diff_eq [simp]: "countable (A - {x}) = countable A"