Nuprl - DiscreteMath LEMMAs for ooc_preserves_dededkind

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

Rank	Theorem	Name
2	Thm* (A ~ B) Dedekind-Infinite(A) Dedekind-Infinite(B)	[ooc_preserves_dededkind_inf]
cites the following:
1	Thm* InvFuns(A;B;f;g) Inj(B; A; g)	[fun_with_inv2_is_inj_rev]
0	Thm* Inj(A; B; g) Inj(B; C; f) Inj(A; C; f o g)	[comp_preserves_inj]
0	Thm* InvFuns(A;B;f;g) Inj(A; B; f)	[fun_with_inv2_is_inj]

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