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

### Proof of a lemma for the Pigeon-hole principle

Show Thm*  m:f:(m). Inj(mf (x:my:xf(x) = f(y)).

That is, given a non-injective assigment of integers to a finite collection we can find two objects (with the second objects y preceding the first value x) that are assigned the same value.
This reduces to showing the contrapositive, namely

(x:my:xf(x) = f(y))  Inj(mf)

(computationally, since there are only finitely many choices for x and y in the specified domain, one could just exhaustively try them all and see if there is a pair whose assignments by f agree).
So assuming that

 (1) (x:m, y:x. f(x) = f(y))

and employing the definition

Def  Inj(ABf) == a1,a2:Af(a1) = f(a2 B  a1 = a2

our proof reduces to showing that if

 (2) f(a1) = f(a2)

then a1 = a2. This further reduces to showing that

a1<a2 & a2<a1

which each follow from assumptions (1) and (2).

QED

This is a lemma for a proof of the pigeon-hole principle

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

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