(7steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
The k-tuples of natural numbers can be placed in one-to-one correspondence with the natural numbers theselves.

At: card nat vs nat tuple

  k:. (k) ~ 
By: NSubsetInd Concl

Generated subgoals:

1 1. k : 
2. 0<k
3. 1 = k
  (k) ~ 
1 step
2 1. k : 
2. 1<k
3. ((k-1)) ~ 
  (k) ~ 
5 steps

About:
natural_numberfunctionall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(7steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc