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
We shall still use a function to express a correspondence, so we must still find a way to characterize which functions from
Consider a function
Def Surj(A; B; f) == b:B. a:A. f(a) = b
I.e., every member of
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
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
About: