| | Some definitions of interest. |
|
| connect | Def x-the_graph- > *y ==  p:Vertices(the_graph) List. path(the_graph;p) & p[0] = x & last(p) = y |
| | | Thm* For any graph
 x,y:V. x-the_graph- > *y  Prop |
|
| path | Def path(the_graph;p) == 0 < ||p|| & (i: (||p||-1). p[i]-the_graph- > p[(i+1)]) |
| | | Thm* For any graph
p:V List. path(the_graph;p) Prop |
|
| edge | Def x-the_graph- > y == e:Edges(the_graph). Incidence(the_graph)(e) = < x,y > |
| | | Thm* For any graph
x,y:V. x-the_graph- > y Prop |
|
| gr_v | Def Vertices(t) == 1of(t) |
| | | Thm* t:Graph. Vertices(t) Type |
|
| graph | Def Graph == v:Type e:Type(e  vv)Top |
| | | Thm* Graph Type{i'} |
