Nuprl - DiscreteMath LEMMAs for one_one_corr_rel_vs

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

Rank	Theorem	Name
2	Thm* R:(ABProp). Thm* (1-1-Corr x:A,y:B. R(x;y)) Thm* Thm* (f:(AB), g:(BA). Thm* (InvFuns(A;B;f;g) & (x:A, y:B. R(x;y) y = f(x) & x = g(y)))	[one_one_corr_rel_vs_invfuns]
cites the following:
1	Thm* (x:A. !y:B(x). P(x;y)) (f:(x:AB(x)). x:A. P(x;f(x)))	[fun_description]
0	Thm* P:(AProp). (!u:A. P(u)) (y,z:A. P(y) P(z) y = z)	[exists_unique_elim]

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