Content deleted Content added
Changed order of reasons for contradiction to clarify. This is a more logical order as it's clear to see xi cannot be in f(xi) to get B at first glance, then leading to the next contradictory statement. |
Electro blob (talk | contribs) No edit summary Tag: Reverted |
||
Line 38:
Despite the simplicity of the above proof, it is rather difficult for an [[automated theorem prover]] to produce it. The main difficulty lies in an automated discovery of the Cantor diagonal set. [[Lawrence Paulson]] noted in 1992 that [[Otter (theorem prover)|Otter]] could not do it, whereas [[Isabelle (proof assistant)|Isabelle]] could, albeit with a certain amount of direction in terms of tactics that might perhaps be considered cheating.<ref name="Paulson1992"/>
[[File:Cantor's Theorem Visual|thumb|A visual showing the two possible ways x could map to its image. In neither case can it map to B. Green arrows represent possible mappings and red arrows impossible mappings.]]
==When ''A'' is countably infinite==
Let us examine the proof for the specific case when <math>A</math> is [[countably infinite]]. [[Without loss of generality]], we may take {{math|1=''A'' = '''N''' = {{mset|1, 2, 3, …}}}}, the set of [[natural number]]s.
| |||