WhoCites
Definitions
HOLlib
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites onto?
onto
Def onto(
'a
;
'b
;
f
) ==
y
:
'b
.
x
:
'a
.
y
=
f
(
x
)
Thm*
'a
,
'b
:Type,
f
:(
'a
'b
). onto(
'a
;
'b
;
f
)
Prop
Syntax:
onto(
'a
;
'b
;
f
)
has structure:
onto(
'a
;
'b
;
f
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
HOLlib
Sections
NuprlLIB
Doc
y:'b. 
x:'a. y = f(x)'a,'b:Type, f:('a
'b). onto('a;'b;f) 
Propy:'b. x:'a. y = f(x)'a,'b:Type, f:('a'b). onto('a;'b;f) Prop
