src/HOL/Library/ContNotDenum.thy
changeset 40702 cf26dd7395e4
parent 37765 26bdfb7b680b
child 53372 f5a6313c7fe4
     1.1 --- a/src/HOL/Library/ContNotDenum.thy	Wed Nov 24 10:52:02 2010 +0100
     1.2 +++ b/src/HOL/Library/ContNotDenum.thy	Mon Nov 22 10:34:33 2010 +0100
     1.3 @@ -565,8 +565,7 @@
     1.4    shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
     1.5  proof -- "by contradiction"
     1.6    assume "\<exists>f::nat\<Rightarrow>real. surj f"
     1.7 -  then obtain f::"nat\<Rightarrow>real" where "surj f" by auto
     1.8 -  hence rangeF: "range f = UNIV" by (rule surj_range)
     1.9 +  then obtain f::"nat\<Rightarrow>real" where rangeF: "surj f" by auto
    1.10    -- "We now produce a real number x that is not in the range of f, using the properties of newInt. "
    1.11    have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
    1.12    moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)