DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
10
Thm*
a
,
b
:
. (
a
b
) ~
(
b
a
)
[card_fun_vs_nsub_exp]
cites the following:
9
Thm*
a
:
,
b
:(
a
). (
i
:
a
b
(
i
)) ~
(
i
:
a
.
b
(
i
))
[card_pi_vs_nsub_pi]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
DiscreteMath
Sections
DiscrMathExt
Doc
a,b:
. (a
b) ~ (b
a)a:, b:(a). (i:ab(i)) ~ (
i:a. b(i))a,b:. (ab) ~ (ba)a:, b:(a). (i:ab(i)) ~ ( i:a. b(i))