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