(35steps 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
exteq
nsub
surj
k
:
. (
k
inj
k
) =ext (
k
onto
k
)
By:
Auto
Generated subgoal:
1
1.
k
:
(
k
inj
k
) =ext (
k
onto
k
)
34
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(35steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
k:
. (k inj
k) =ext (k onto k) k:. (k inj k) =ext (k onto k)
(k inj k) =ext (k onto k)
