Mon, 08 Aug 2016 18:52:09 +0200
changeset 63628 d02601840466
parent 63625 1e7c5bbea36d
child 63629 3b3ab4674274
--- 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.
 theorem real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"