(31steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
The cardinality of injections on a finite nonempty domain in terms of injections on a domain one smaller.

The number ways to order a distinct objects from among b is b times the number of ways to order a-1 distinct objects from among b-1.

At: card nsub inj vs lopped

  a,b:. (a inj b) ~ (b((a-1) inj (b-1)))
By: Auto

Generated subgoal:

1 1. a : 
2. b : 
  (a inj b) ~ (b((a-1) inj (b-1)))
30 steps

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

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