(2steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
nsub
inj
ooc
nsub
surj
k
:
. (
k
inj
k
) ~ (
k
onto
k
)
By:
SimilarTo
Thm*
(
k
inj
k
) =ext (
k
onto
k
)
Generated subgoal:
1
1.
k
:
2. (
k
inj
k
) =ext (
k
onto
k
)
(
k
inj
k
) ~ (
k
onto
k
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
k:
. (k inj
k) ~ (k onto k) k:. (k inj k) ~ (k onto k)k inj k) =ext (k onto k)
k inj k) =ext (k onto k)
(k inj k) ~ (k onto k)
