DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def  A onto B == {f:(AB)| Surj(ABf) }

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*  (a:f:(a onto B). (y.least x:. (f(x)) e y B inj a)
Thm*  (A ~ A' (B ~ B' ((A onto B) ~ (A' onto B'))[surjection_type_functionality_wrt_ooc]
Thm*  f:(a onto b). Surj(abf)[surjection_type_nsub_surjection]
Thm*  f:(A onto B), a:a onto A  (B Discrete)  Surj(ABf)[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:bf(least x:f(x)=y) = y[nsub_surj_least_preimage_works]
Thm*  e:(BB). 
Thm*  IsEqFun(B;e (a:f:(a onto B), y:Bf(least x:. (f(x)) e y) = y)
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)
Thm*  (A Discrete)  (k:f:(kA). f  k onto {a:Ai:ka = 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

DiscreteMath Sections DiscrMathExt Doc