Hi Brian,
it's great that you are interested in graph theory. Although I work only
with undirected graphs (at the monment), the definitions in 16.1 should be
general enough to be used also for other kinds of graphs.
A definition for directed pseudographs (allowing multiedges and loops)
could be (analogous to the definition df-upgr for undirected pseudographs):
df-dpgr $a |- DPGraph = { g | [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e
]. e : dom e --> ( v X. v ) } $.
If you want to have directed multigraphs (pseudographs without loops), you
could define them as follows:
df-dmgr $a |- DMGraph = { g | [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ].
e : dom e --> { x e. ( v X. v ) | ( 1st ` x ) =/= ( 2nd ` x ) } } $.
The other conditions you listed would be more complicated to formalize.
Maybe the start and end vertices could be modelled by providing an ordered
set (maybe Words) as domain of the edge function e, and the first vertex of
the first edge and the second vertex of the last edge could be regarded as
start vertex resp. end vertex.
I hope these hints are sufficient for you to continue.
Alexander
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/987aacd4-de44-42fb-9ea4-6819da2b6024n%40googlegroups.com.
