Proof of the Pigeon-hole principle

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

That is, putting a finite collection of m objects into fewer pigeon-holes (k<m) means there are two distinct objects put into the same hole. Without loss of generality it is enough that

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

i.e. that the second object y precedes the first object x. By a lemma

Thm*  m:, f:(m). Inj(m; ; f)  (x:m, y:x. f(x) = f(y))

Gloss

it is enough to show that

Inj(m; ; f)

(since f  mk automatically puts f  m as well).

But according to our core lemma

Thm*  (f:(mk). Inj(m; k; f))  mk

Gloss

Inj(m; ; f) would contradict our assumption that k<m, hence

Inj(m; ; f).

QED

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