PfPrintForm Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Proof of a Fundamental theorem for Finite Injections

Show Thm*  (f:(mk). Inj(mkf))  mk.

This will be proved using induction on m, varying k.
The base case, 0k, is trivial, so we move on to the induction step, assuming 0<m, and assuming the induction hypothesis:

k':. (f':((m-1)k'). Inj((m-1); k'f'))  m-1k'.

The problem is then to show that mk, given some f  mk such that Inj(mkf).

Obviously, mk will follow from m-1k-1, so by applying the induction hyp to k-1, our problem reduces to finding an f'  (m-1)(k-1) such that Inj((m-1); (k-1); f').
Such a construction is

Def  Replace value k by f(m) in f == Replace values x s.t. x=k by f(m) in f

Def  (Replace values x s.t. P(x) by y in f)(i) == if P(f(i)) y else f(i) fi

Thm*  Inj((m+1); (k+1); f Inj(mk; Replace value k by f(m) in f)

This last theorem is sufficient for concluding our argument.

Note: Considering f  (k+1)(j+1) as a sequence of k+1 values selected from the first j+1 natural numbers,
(Replace value j by f(k) in f kj removes the entry for the largest value, namely j, and replaces it with the last value of the sequence, namely f(k), if necessary.

This is the key lemma to the proofs of the uniqueness of counting, and the pigeon-hole principle, i.e.,

Thm*  (A ~ m (A ~ k m = k


Thm*  m,k:f:(mk). k<m  (x,y:mx  y & f(x) = f(y))


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

PfPrintForm Definitions DiscreteMath Sections DiscrMathExt Doc