DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
8
Thm*
(
k
inj
k
) ~ (
k
onto
k
)
[nsub_inj_ooc_nsub_surj]
cites the following:
7
Thm*
(
k
inj
k
) =ext (
k
onto
k
)
[nsub_inj_exteq_nsub_surj]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
DiscreteMath
Sections
DiscrMathExt
Doc
k inj
k) ~ (k onto k)k inj k) =ext (k onto k)k inj k) ~ (k onto k)k inj k) =ext (k onto k)