DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
TheoremName
Thm*  InvFuns(A;B;f;g Surj(BAg)[fun_with_inv2_is_surj_rev]
cites the following:
Thm*  InvFuns(A;B;f;g InvFuns(B;A;g;f)[inv_funs_2_sym]
Thm*  InvFuns(A;B;f;g Surj(ABf)[fun_with_inv2_is_surj]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
DiscreteMath Sections DiscrMathExt Doc