(11steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
The size of the general product space (whose members are functions) of a finite family of finite classes is the integer product of those classes' sizes.

At: card pi vs nsub pi

  a:, b:(a). (i:ab(i)) ~ ( i:a. b(i))
By: NatInd Concl

Generated subgoals:

1 1. b : 0
  (i:0b(i)) ~ ( i:0. b(i))
5 steps
2 1. a : 
2. 0<a
3. b:((a-1)). (i:(a-1)b(i)) ~ ( i:(a-1). b(i))
4. b : a
  (i:ab(i)) ~ ( i:a. b(i))
5 steps

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

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