src/HOL/Rat.thy
changeset 57275 0ddb5b755cdc
parent 57136 653e56c6c963
child 57512 cc97b347b301
     1.1 --- a/src/HOL/Rat.thy	Wed Jun 18 15:23:40 2014 +0200
     1.2 +++ b/src/HOL/Rat.thy	Wed Jun 18 07:31:12 2014 +0200
     1.3 @@ -916,6 +916,8 @@
     1.4    "q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q"
     1.5    by (rule Rats_cases) auto
     1.6  
     1.7 +lemma Rats_infinite: "\<not> finite \<rat>"
     1.8 +  by (auto dest!: finite_imageD simp: inj_on_def infinite_UNIV_char_0 Rats_def)
     1.9  
    1.10  subsection {* Implementation of rational numbers as pairs of integers *}
    1.11