(9steps 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 a general sum (whose members are pairs) of a finite family of finite classes is the integer sum of those classes' sizes.

At: card sigma vs nsub sigma

  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))
4 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))
4 steps

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

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