The file 'cantor.v' as Latin-1 text
1 Definition enumeration: Type := nat -> (nat-> nat).
2 Definition diagonal (g: enumeration) (n: nat): nat := g n n.
3 Definition different (f: nat->nat) (g: nat->nat): Prop := exists n: nat, f(n)<>g(n).
4
5 Theorem cantor : forall g: enumeration, exists f: nat->nat,
6 forall i: nat, different (g i) f.
7 intro. (* Let g be an enumeration of all functions. *)
8 exists (fun k=>S(diagonal g k)).
9 intro. (* Let i be a row--an element of the enumeration. *)
10 exists i.
11 auto.
12 Qed.