(5steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
nsub
surj
exteq
nsub
bij
k
:
. (
k
onto
k
) =ext (
k
bij
k
)
By:
Auto THEN New:
f
(2 Times Analyze)
Generated subgoals:
1
1.
k
:
2.
f
:
k
onto
k
f
k
bij
k
3
steps
2
1.
k
:
2.
f
:
k
bij
k
f
k
onto
k
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
k:
. (k onto
k) =ext (k bij k) k:. (k onto k) =ext (k bij k)
k onto k
f 
k bij k
k bij k
f k onto k
