(2steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
compose
wf
surj
A
,
B
,
C
:Type,
f
:(
B
onto
C
),
g
:(
A
onto
B
).
f
o
g
A
onto
C
By:
UnivCD THEN Analyze-1 THEN Analyze4 THEN Analyze
Generated subgoal:
1
1.
A
: Type
2.
B
: Type
3.
C
: Type
4.
f
:
B
C
5. Surj(
B
;
C
;
f
)
6.
g
:
A
B
7. Surj(
A
;
B
;
g
)
Surj(
A
;
C
;
f
o
g
)
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
A,B,C:Type, f:(B onto
C), g:(A onto B). f o g 
A onto C A,B,C:Type, f:(B onto C), g:(A onto B). f o g A onto C
C
B
Surj(A; C; f o g)
