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

is mentioned by

Thm*  Bij(A; B; f)  f is 1-1 corr	[bij_iff_is_1_1_corr]
Def  f is permutation on A == f is 1-1 corr	[is_permutation]

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html