DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
10
Thm*
p
:(
a
{
k
}
). {
i
:
a
|
p
(
i
) } ~
k
[card_st_sized_bool]
cites the following:
9
Thm*
p
:(
a
). {
x
:
a
|
p
(
x
) } ~
(
size(
a
)(
p
))
[card_st_vs_boolsize]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
DiscreteMath
Sections
DiscrMathExt
Doc
p:(
a {k}
). {i:a| p(i) } ~ kp:(a
). {x:a| p(x) } ~ (size(a)(p))p:(a {k} ). {i:a| p(i) } ~ kp:(a). {x:a| p(x) } ~ (size(a)(p))