Nuprl - DiscreteMath LEMMAs for injection_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 inj B) ~ (A' inj B'))	[injection_type_functionality_wrt_ooc]
cites the following:
1	Thm* InvFuns(A;B;f;g) Inj(A; B; f) & Inj(B; A; g)	[invfuns_are_inj]
0	Thm* Inj(A; B; g) Inj(B; C; f) Inj(A; C; f o g)	[comp_preserves_inj]

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