equal
deleted
inserted
replaced
563 |
563 |
564 theorem real_non_denum: |
564 theorem real_non_denum: |
565 shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)" |
565 shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)" |
566 proof -- "by contradiction" |
566 proof -- "by contradiction" |
567 assume "\<exists>f::nat\<Rightarrow>real. surj f" |
567 assume "\<exists>f::nat\<Rightarrow>real. surj f" |
568 then obtain f::"nat\<Rightarrow>real" where "surj f" by auto |
568 then obtain f::"nat\<Rightarrow>real" where rangeF: "surj f" by auto |
569 hence rangeF: "range f = UNIV" by (rule surj_range) |
|
570 -- "We now produce a real number x that is not in the range of f, using the properties of newInt. " |
569 -- "We now produce a real number x that is not in the range of f, using the properties of newInt. " |
571 have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast |
570 have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast |
572 moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter) |
571 moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter) |
573 ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast |
572 ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast |
574 moreover from rangeF have "x \<in> range f" by simp |
573 moreover from rangeF have "x \<in> range f" by simp |