--- a/src/HOL/Library/Countable.thy Tue Jun 26 15:44:35 2018 +0100
+++ b/src/HOL/Library/Countable.thy Tue Jun 26 17:22:43 2018 +0200
@@ -56,7 +56,7 @@
proof
have "finite (UNIV::'a set)" by (rule finite_UNIV)
with finite_conv_nat_seg_image [of "UNIV::'a set"]
- obtain n and f :: "nat \<Rightarrow> 'a"
+ obtain n and f :: "nat \<Rightarrow> 'a"
where "UNIV = f ` {i. i < n}" by auto
then have "surj f" unfolding surj_def by auto
then have "inj (inv f)" by (rule surj_imp_inj_inv)
@@ -323,4 +323,7 @@
qed
qed
+theorem rat_denum: "\<exists>f :: nat \<Rightarrow> rat. surj f"
+ using surj_nat_to_rat_surj by metis
+
end