One-to-One Correspondence via Bijection

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

Here we shall give a different, and to some readers more natural, "definition" of the expression (f is 1-1 corr).

We shall still use a function to express a correspondence, so we must still find a way to characterize which functions from AB are one-to-one, but we shall do so in a more descriptive way than to stipulate that there is an inverse function.

Consider a function f  AB that is supposed to match A and B member-for-member. Every member of A gets paired with some member of B, but there are a couple of things that might go wrong. First, we might miss some member of B; so a one-to-one correspondence must be what we shall call a "surjection":

Def  Surj(A; B; f) == b:B. a:A. f(a) = b

I.e., every member of B is reachable through f from some member of A.

The other way that a function could fail to match two classes one-to-one is if it paired two different members of one class against just one member of the other. Of course, a function can only pair one value with each argument, but in general could have the same value for different arguments, so this is what must be excluded. We call a function having a unique argument for each value an injection, and define it thus:

Def  Inj(A; B; f) == a1,a2:A. f(a1) = f(a2)  B  a1 = a2

I.e., if the outputs are equal, then the inputs are equal.

A function having both of these properties, and so one that is a one-to-one correspondence, is called a bijection:

Def  Bij(A; B; f) == Inj(A; B; f) & Surj(A; B; f)

So, if we had not already defined (f is 1-1 corr) we could define it as being a bijection, i.e., Bij(A; B; f)

This situation is typical of making definitions. Still, we can approximate making a second definition simply by showing that

Thm*  Bij(A; B; f)  f is 1-1 corr

For a discussion of this theorem and the alternative characterizations see Bijection vs Inverses.

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