A finite non-injection into integers maps some two distinct arguments to the same value.

At: finite inj counter example

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

1

1. m :  2. f : m 3. Inj(m; ; f)   x:m, y:x. f(x) = f(y)

5 steps

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