# HG changeset patch
# User kleing
# Date 1530026563 -7200
# Node ID a8ada04583e7637566dca2cce78e69e4c373b453
# Parent  8a8f98c84df3cb9939c516e2d99c958c8b3e2735
more explicit statement of rat_denum to fit with top100 thms list

diff -r 8a8f98c84df3 -r a8ada04583e7 src/HOL/Library/Countable.thy
--- 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