src/HOL/Library/Continuum_Not_Denumerable.thy

 text \<open>
   The following document presents a proof that the Continuum is uncountable.
   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.
 
   First we formalise some properties of closed intervals, then we prove the

   Real numbers and is the foundation for our argument. Informally it states
   that an intersection of countable closed intervals (where each successive
   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"
 proof
   assume "\<exists>f::nat \<Rightarrow> real. surj f"