mb
nat
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
4
Thm*
n
,
m
:
,
f
:(
n
m
). Inj(
n
;
m
;
f
)
n
m
[pigeon-hole]
cites the following:
3
Thm*
n
,
k
:
,
c
:(
n
k
).
Thm*
p
:(
k
(
List)).
Thm*
sum(||
p
(
j
)|| |
j
<
k
) =
n
Thm*
& (
j
:
k
,
x
,
y
:
||
p
(
j
)||.
x
<
y
(
p
(
j
))[
x
]>(
p
(
j
))[
y
])
Thm*
& (
j
:
k
,
x
:
||
p
(
j
)||. (
p
(
j
))[
x
]<
n
&
c
((
p
(
j
))[
x
]) =
j
)
[finite-partition]
0
Thm*
k
,
b
:
,
f
:(
k
). (
x
:
k
.
f
(
x
)
b
)
sum(
f
(
x
) |
x
<
k
)
b
k
[sum_bound]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb
nat
Sections
MarkB
generic
Doc