(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
1
2
1
1
1
1
1
1.
k
:
2.
f
:
k
onto
k
3.
f
k
k
4. Surj(
k
;
k
;
f
)
5.
X
:
k
6.
a
:
k
7.
f
(
X
) =
f
(
a
)
8.
X
=
a
({
x
:
k
|
x
=
X
} onto
k
)
By:
Def THEN UseWitness
f
THEN Analyze
Generated subgoals:
1
f
{
x
:
k
|
x
=
X
}
k
1
step
2
Surj({
x
:
k
|
x
=
X
};
k
;
f
)
5
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