Proof of a lemma for the Pigeon-hole principle

Thm*  m:, f:(m). Inj(m; ; f)  (x:m, y:x. f(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:m, y:x. f(x) = f(y))  Inj(m; ; f)

(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(A; B; f) == a1,a2:A. f(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:m. x  y & f(x) = f(y))

Gloss

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