One-to-One Correspondence: equivalence of two characterizations.

This discussion continues from the introductions of an alternative definition of one-to-one correspondence

We have given three "definitions" of sorts to the concept of one-to-one correspondence between two classes, symbolized as *A* ~~ *B*

We gave a suggestive description of the concept informally, then gave a different equivalent description interms of the existence of inverse functions, then a third explanation was in terms of the existence of bijections. In order make reasoning about *A* ~~ *B**A* ~~ *B*

When there are several candidates for defining the new relation, it is typical to pick one as the principle definition, and demonstrate the equivalence of the others. In our case, we chose to use

Def A~~B==f:(AB),g:(BA). InvFuns(A;B;f;g)

As the principle definition and prove

Thm* ( f:(AB). Bij(A;B;f)) (A~B)

as a theorem, although we could just as easily have chosen the reverse. The "use" of this theorem will be pretty much as if it were a definition of *A* ~~ *B*

If you trace down the definitions of *A*; *B*; *f*)*A* ~~ *B*

Examination of the proof will reveal that it reduces to two lemmas expression the opposite directions of implication, namely,

Thm* f:(AB). Bij(A;B;f) (g:(BA). InvFuns(A;B;f;g))

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

The proof of the first theorem shows how to construct an inverse of a function given it's a bijection. The second uses the inverse of a function to show its a bijection.

About: