Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
one_one_corr_2
Def
A
~
B
==
f
:(
A
B
),
g
:(
B
A
). InvFuns(
A
;
B
;
f
;
g
)
Thm*
A
,
B
:Type. (
A
~
B
)
Prop
singleton
Def
{
a
:
T
} == {
x
:
T
|
x
=
a
T
}
Thm*
T
:Type,
a
:
T
. {
a
:
T
}
Type
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
f:(A
B), g:(BA). InvFuns(A;B;f;g)
A,B:Type. (A ~ B) 
Prop T }T:Type, a:T. {a:T} Typef:(AB), g:(BA). InvFuns(A;B;f;g)A,B:Type. (A ~ B) Prop T }T:Type, a:T. {a:T} Type
