Nuprl - DiscreteMath LEMMAs for nsub_surj_imp_a_rev_inj

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

Rank	Theorem	Name
3	Thm* e:(BB). Thm* IsEqFun(B;e) Thm* Thm* (a:, f:(a onto B). (y.least x:. (f(x)) e y) B inj a)	[nsub_surj_imp_a_rev_inj_gen]
cites the following:
2	Thm* e:(BB). Thm* IsEqFun(B;e) (a:, f:(a onto B), y:B. (least x:. (f(x)) e y) a)	[nsub_surj_least_preimage_total_gen]
2	Thm* e:(BB). Thm* IsEqFun(B;e) (a:, f:(a onto B), y:B. f(least x:. (f(x)) e y) = y)	[nsub_surj_least_preimage_works_gen]

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