mb
nat
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
2
Thm*
m
,
n
,
k
:
,
f
:(
n
m
),
g
:(
k
m
).
Thm*
increasing(
f
;
n
)
Thm*
Thm*
increasing(
g
;
k
)
Thm*
Thm*
(
i
:
m
. (
j
:
n
.
i
=
f
(
j
))
(
j
:
k
.
i
=
g
(
j
)))
Thm*
Thm*
(
j1
:
n
,
j2
:
k
.
f
(
j1
) =
g
(
j2
))
m
=
n
+
k
[disjoint_increasing_onto]
cites the following:
1
Thm*
k
,
m
:
. (
f
:(
k
m
). Inj(
k
;
m
;
f
))
k
m
[injection_le]
1
Thm*
k
,
m
:
,
f
:(
k
m
). increasing(
f
;
k
)
Inj(
k
;
m
;
f
)
[increasing_inj]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb
nat
Sections
MarkB
generic
Doc