WhoCites
Definitions
MarkB
generic
Sections
NuprlLIB
Doc
Who Cites int
iseg?
int_iseg
Def {i...j} == {k:
| i
k & k
j }
Thm*
i,j:
. {i...j}
Type
le
Def
A
B ==
B < A
Thm*
i,j:
. (i
j)
Prop
not
Def
A == A
False
Thm*
A:Prop. (
A)
Prop
Syntax:
{i...j}
has structure:
int_iseg(i; j)
About:
WhoCites
Definitions
MarkB
generic
Sections
NuprlLIB
Doc