WhoCites
Definitions
StandardLib
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites inject?
inject
Def Inj(
A
;
B
;
f
) ==
a1
,
a2
:
A
.
f
(
a1
) =
f
(
a2
)
B
a1
=
a2
Thm*
A
,
B
:Type,
f
:(
A
B
). Inj(
A
;
B
;
f
)
Prop
Syntax:
Inj(
A
;
B
;
f
)
has structure:
inject(
A
;
B
;
f
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
StandardLib
Sections
NuprlLIB
Doc
a1,a2:A. f(a1) = f(a2) 
B 
a1 = a2A,B:Type, f:(A
B). Inj(A; B; f) Propa1,a2:A. f(a1) = f(a2) B a1 = a2A,B:Type, f:(AB). Inj(A; B; f) Prop
