cantor.v

  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.