Alexander van der Vekens contributed an impressive collection of definitions and theorems for graph theory. Most of it applies to undirected hypergraphs, but most of 16.1 seems generally applicable.
I want to model a directed binary graph, G, that has many of the properties of a poset, but has a partial order relation which is irreflexive, ( lt ` f ) rather than ( le ` f ). I need graph G = <. V , E >. where V is a set of vertices, and E is a set of binary, directed edges on V, E C_ ( V x V ) where the direction is from the first element of the ordered pair, to the second element, with the following properties: - E must connect V - E must be acyclic - E must have a distinguished "start" vertex (least vertex l e. V), from which there must be a path to every other vertex in V - E must have a distinguished "end" vertex (upper bound u e. V), to which there must be a path from every other vertex in V - Existence of a path from V1 to V2 determines V1 < V2 df-vtx and df-iedg look like a good start to represent vertices and edges as extensible structures. However, these properties of E look like a poset with lt derived from le by df-plt. How do I require edges E to also be a poset with V = ( Base ` E ) and ( lt ` E ) defined as path existence? Does G being connected follow from ( E e. Poset )? --Brian -- 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/336951a7-37fe-4709-806b-2efd039480ben%40googlegroups.com.
