DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
2
Thm*
(
A
~
B
)
(
B
~
A
)
[one_one_corr_2_inversion]
cites the following:
1
Thm*
EquivRel
X
,
Y
:Type.
X
~
Y
[one_one_corr_is_equiv_rel]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
DiscreteMath
Sections
DiscrMathExt
Doc
(B ~ A) (B ~ A)