WhoCites
Definitions
mb
list
2
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites nondecreasing?
nondecreasing
Def nondecreasing(
f
;
k
) ==
i
:
(
k
-1).
f
(
i
)
f
(
i
+1)
int_seg
Def
{
i
..
j
} == {
k
:
|
i
k
<
j
}
Thm*
m
,
n
:
. {
m
..
n
}
Type
lelt
Def
i
j
<
k
==
i
j
&
j
<
k
le
Def
A
B
==
B
<
A
Thm*
i
,
j
:
. (
i
j
)
Prop
not
Def
A
==
A
False
Thm*
A
:Prop. (
A
)
Prop
Syntax:
nondecreasing(
f
;
k
)
has structure:
nondecreasing(
f
;
k
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
mb
list
2
Sections
MarkB
generic
Doc