One-to-One Correspondence via Inverse Functions

One observation is that when a function f  AB matches A and B member-for-member, then one can reverse this function to get some g  BA which matches these classes in the opposite direction. When functions f and g have this inverse relation between them, we say they are "inverses" and write InvFuns(A;B;f;g). We define this relation between functions as

Def  InvFuns(A;B;f;g) == (x:A. g(f(x)) = x) & (y:B. f(g(y)) = y)

Notice that this inverse relation between functions is symmetric, i.e.,

Thm*  InvFuns(A;B;f;g)  InvFuns(B;A;g;f)

(just swap the conjuncts in the def)

Cancellation

When in the course of reasoning one uses the fact that (g(f(x)) = x) to rewrite g(f(x)) to x, this is sometimes called "cancellation" of f by g. Inverse functions cancel each other. For example, subtracting an integer (from something) and adding that same integer are inverse functions, so you may use one to cancel the other, by rewriting x-a+a or x+a-a to x.

Uniqueness

As you can imagine, if a function has an inverse, that inverse is unique.
Here is a theorem to that effect:

Thm*  InvFuns(A;B;f;g)  InvFuns(A;B;f;h)  g = h

As usual, some persons who have doubts about our choice of definition for InvFuns(A;B;f;g) might use this fact as further justification of the definition; whereas those who already find the definition adequate might use the proof either to complement the imagination, or resolve doubts about uniqueness.

We adopt the following definition of one-to-one correspondence:

Def  f is 1-1 corr == g:(BA). InvFuns(A;B;f;g)

There is another characterization of one-to-one correspondence, involving "bijection", which may well seem more obviously right. To follow this development, see One-to-One Correspondence via Bijection.

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