# HG changeset patch # User wenzelm # Date 1470675129 -7200 # Node ID d02601840466b35519f3483e4f30ab949a42e1c0 # Parent 1e7c5bbea36dd2dd56705630f8e456de91b9788a tuned; diff -r 1e7c5bbea36d -r d02601840466 src/HOL/Library/Continuum_Not_Denumerable.thy --- 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>\Theorem:\ The Continuum \\\ is not denumerable. In other words, there does - not exist a function \f: \ \ \\ such that f is surjective. + not exist a function \f: \ \ \\ such that \f\ is surjective. \<^bold>\Outline:\ 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 \f: \ \ \\ exists and find a real \x\ such that \x\ is not in the range of \f\ by generating a sequence of closed intervals then using the - NIP. + Nested Interval Property. \ theorem real_non_denum: "\f :: nat \ real. surj f"