more explicit statement of rat_denum to fit with top100 thms list
authorkleing
Tue Jun 26 17:22:43 2018 +0200 (14 months ago)
changeset 68502a8ada04583e7
parent 68501 8a8f98c84df3
child 68515 0854edc4d415
more explicit statement of rat_denum to fit with top100 thms list
src/HOL/Library/Countable.thy
     1.1 --- a/src/HOL/Library/Countable.thy	Tue Jun 26 15:44:35 2018 +0100
     1.2 +++ b/src/HOL/Library/Countable.thy	Tue Jun 26 17:22:43 2018 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4  proof
     1.5    have "finite (UNIV::'a set)" by (rule finite_UNIV)
     1.6    with finite_conv_nat_seg_image [of "UNIV::'a set"]
     1.7 -  obtain n and f :: "nat \<Rightarrow> 'a" 
     1.8 +  obtain n and f :: "nat \<Rightarrow> 'a"
     1.9      where "UNIV = f ` {i. i < n}" by auto
    1.10    then have "surj f" unfolding surj_def by auto
    1.11    then have "inj (inv f)" by (rule surj_imp_inj_inv)
    1.12 @@ -323,4 +323,7 @@
    1.13    qed
    1.14  qed
    1.15  
    1.16 +theorem rat_denum: "\<exists>f :: nat \<Rightarrow> rat. surj f"
    1.17 + using surj_nat_to_rat_surj by metis
    1.18 +
    1.19  end