fun 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def Bij(A; B; f) == Inj(A; B; f) & Surj(A; B; f)

is mentioned by

Thm* (f:(AB). Bij(A; B; f))  (A ~~ B)[bij_iff_1_1_corr]
Thm* f:(AB), g:(BA). InvFuns(A; B; f; g)  Bij(A; B; f)[fun_with_inv_is_bij]
Thm* f:(AB). Bij(A; B; f)  (g:(BA). InvFuns(A; B; f; g))[bij_imp_exists_inv]

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

fun 1 Sections StandardLIB Doc