(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
1
1.
k
:
2.
f
:
k
onto
k
f
k
bij
k
By:
f
k
inj
k
Asserted THENA BackThru:
Thm*
(
k
inj
k
) =ext (
k
onto
k
)
Generated subgoal:
1
3.
f
k
inj
k
f
k
bij
k
2
steps
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 onto
k
f 
k bij k
k onto k
f k bij k k inj k Asserted THENA BackThru: Thm* (k inj k) =ext (k onto k) k inj k
f k bij k
