PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Equivalence of two forms of relational one-to-one correspondence
At:
rel
1
1
eq
rel
1
1
b
A
,
B
,
A
,
B
:Type,
R
:(
A
B
Prop). (
R
is 1-1) = (1-1
x
A
,
y
B
.
R
(
x
;
y
))
By:
ReduceSOAps Concl THEN Def
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
A,B,A,B:Type, R:(A
BProp). (R is 1-1) = (1-1 x
A,yB. R(x;y)) A,B,A,B:Type, R:(ABProp). (R is 1-1) = (1-1 xA,yB. R(x;y))
