Nuprl - Proof: pigeon hole

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
The pigeon-hole principle

A mapping from one finite collection into a smaller collection assigns a single output to two inputs.

m,k:

, f:(

k). k<m

(

x,y:

m. x

y & f(x) = f(y))

By:

Auto

Generated subgoal:

1 1. m :
2. k :
3. f : mk
4. k<m
x,y:m. x y & f(x) = f(y)
7 steps

About:

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