author wenzelm Mon, 08 Aug 2016 18:52:09 +0200 changeset 63628 d02601840466 parent 63625 1e7c5bbea36d child 63629 3b3ab4674274
tuned;
```--- a/src/HOL/Library/Continuum_Not_Denumerable.thy	Sun Aug 07 12:10:49 2016 +0200
+++ b/src/HOL/Library/Continuum_Not_Denumerable.thy	Mon Aug 08 18:52:09 2016 +0200
@@ -16,7 +16,7 @@
It is formalised in the Isabelle/Isar theorem proving system.

\<^bold>\<open>Theorem:\<close> The Continuum \<open>\<real>\<close> is not denumerable. In other words, there does
-  not exist a function \<open>f: \<nat> \<Rightarrow> \<real>\<close> such that f is surjective.
+  not exist a function \<open>f: \<nat> \<Rightarrow> \<real>\<close> such that \<open>f\<close> is surjective.

\<^bold>\<open>Outline:\<close> An elegant informal proof of this result uses Cantor's
Diagonalisation argument. The proof presented here is not this one.
@@ -28,7 +28,7 @@
interval is a subset of the last) is non-empty. We then assume a surjective
function \<open>f: \<nat> \<Rightarrow> \<real>\<close> exists and find a real \<open>x\<close> such that \<open>x\<close> is not in the
range of \<open>f\<close> by generating a sequence of closed intervals then using the
-  NIP.
+  Nested Interval Property.
\<close>

theorem real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"```