WhoCites
Definitions
graph
1
3
Sections
Graphs
Doc
Who Cites adjmatrix?
adjmatrix
Def AdjMatrix == size:
size
size
Thm* AdjMatrix
Type
int_seg
Def
{i..j
} == {k:
| i
k < j }
Thm*
m,n:
. {m..n
}
Type
nat
Def
== {i:
| 0
i }
Thm*
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:
AdjMatrix
has structure:
adjmatrix
About:
WhoCites
Definitions
graph
1
3
Sections
Graphs
Doc