Definitions
fun
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
biject
Def
Bij(
A
;
B
;
f
) == Inj(
A
;
B
;
f
) & Surj(
A
;
B
;
f
)
Thm*
A
,
B
:Type,
f
:(
A
B
). Bij(
A
;
B
;
f
)
Prop
inv_funs
Def
InvFuns(
A
;
B
;
f
;
g
) ==
g
o
f
= Id &
f
o
g
= Id
Thm*
A
,
B
:Type,
f
:(
A
B
),
g
:(
B
A
). InvFuns(
A
;
B
;
f
;
g
)
Prop
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
fun
1
Sections
StandardLIB
Doc
A,B:Type, f:(A
B). Bij(A; B; f) 
PropA,B:Type, f:(AB), g:(BA). InvFuns(A; B; f; g) PropA,B:Type, f:(AB). Bij(A; B; f) PropA,B:Type, f:(AB), g:(BA). InvFuns(A; B; f; g) Prop
