Nuprl - DiscreteMath LEMMAs for surjection_type_functionality_wrt

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Rank	Theorem	Name
2	Thm* (A ~ A') (B ~ B') ((A onto B) ~ (A' onto B'))	[surjection_type_functionality_wrt_ooc]
cites the following:
1	Thm* InvFuns(A;B;f;g) Surj(A; B; f) & Surj(B; A; g)	[invfuns_are_surj]
0	Thm* Surj(A; B; g) Surj(B; C; f) Surj(A; C; f o g)	[comp_preserves_surj]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html