Def  A onto B == {f:(AB)| Surj(A; B; f) }

is mentioned by

Thm*  (k inj k) ~ (k onto k)	[nsub_inj_ooc_nsub_surj]
Thm*  (k onto k) ~ (k bij k)	[nsub_surj_ooc_nsub_bij]
Thm*  (k onto k) =ext (k bij k)	[nsub_surj_exteq_nsub_bij]
Thm*  (k inj k) =ext (k onto k)	[nsub_inj_exteq_nsub_surj]
Thm*  ((a onto b))  ba	[surj_typing_imp_le]
Thm*  ((a onto b))  ((b inj a))	[nsub_surj_imp_a_rev_inj2]
Thm*  f:(a onto b). (y.least x:. f(x)=y)  b inj a	[nsub_surj_imp_a_rev_inj]
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]
Thm*  (A ~ A')  (B ~ B')  ((A onto B) ~ (A' onto B'))	[surjection_type_functionality_wrt_ooc]
Thm*  f:(a onto b). Surj(a; b; f)	[surjection_type_nsub_surjection]
Thm*  f:(A onto B), a:. a onto A  (B Discrete)  Surj(A; B; f)	[surjection_type_surjection]
Thm*  f:(B onto C), g:(A onto B). f o g  A onto C	[compose_wf_surj]
Thm*  (A bij B) ~ ((A inj B)(A onto B))	[bijtype_ooc_inj_isect_surjtype]
Thm*  f:(a onto b), y:b. f(least x:. f(x)=y) = y	[nsub_surj_least_preimage_works]
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]
Thm*  f:(a onto b), y:b. (least x:. f(x)=y)  a	[nsub_surj_least_preimage_total]
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]
Thm*  (A Discrete)  (k:, f:(kA). f  k onto {a:A| i:k. a = f(i) })	[nsub_discr_range_surjtype]
Thm*  (A bij B) =ext ((A inj B)(A onto B))	[bijtype_exteq_inj_isect_surjtype]
Thm*  (A bij B)  (A onto B)	[bijection_type_inc_surj]
Thm*  (A bij B)  (A onto B)	[bijtype_sub_surjtype]

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html