DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
4
Thm*
(
) ~
[card_nat_vs_nat_nat]
cites the following:
3
Thm*
(
f
:(
A
B
). Bij(
A
;
B
;
f
))
(
B
~
A
)
[bij_iff_1_1_corr_version2a]
2
Thm*
Bij(
;
; nat_to_nat_pair)
[nat_to_nat_pair_bij]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
DiscreteMath
Sections
DiscrMathExt
Doc
) ~ 
f:(A
B). Bij(A; B; f)) 
(B ~ A); ; nat_to_nat_pair)) ~ f:(AB). Bij(A; B; f)) (B ~ A); ; nat_to_nat_pair)