Definitions
DiscreteMath
Sections
DiscrMathExt
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
nat
Def
== {
i
:
| 0
i
}
Thm*
Type
nat_to_nat_pair
Def
nat_to_nat_pair(
i
) == next_nat_pair{
i
}(<0,0>)
Thm*
nat_to_nat_pair
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
A,B:Type, f:(A
B). Bij(A; B; f) 
Prop
== {i:
| 0
i } Type
i}(<0,0>) 
A,B:Type, f:(AB). Bij(A; B; f) Prop == {i:| 0i } Typei}(<0,0>) 
