Hi Brian,
here are some additional remarks/hints on your points:
On Friday, December 31, 2021 at 11:58:47 PM UTC+1 [email protected]
wrote:
> Thierry and Alexander,
>
> Thank you for the hints. structtousgr looks like a good example to study.
> I was not aware of the sSet operator. That looks like a good way to
> enforce the partial-order property.
> The definition of E also prevents self-loops.
>
Yes, because, of -. E. z ( x ( le ‘ P ) z /\ z ( le ‘ P ) y ). But this
condition also prevents many Posets to become graphs (at least ones with
edges). For example, the field of the real numbers as Toset (see ~retos)
would become a graph with no edges, because for every x,y there is a z with
( x ( le ‘ P ) z /\ z ( le ‘ P ) y . An alternative definition for the
edges could be E = { <. x, y >. | x ( lt ‘ P ) y }, but this would result
in much more edges (not only edges between direct neighbors regarding the
order relation).
> I'd also add existential uniqueness to disallow multiedges.
>
This is not necessary, because by choosing ( _I |` E ) as edge function
(the edges are indexed by themselves), there is no way to have multiedges (
( _I |` E ) is a 1-1 function, see ~f1oi)
Least and greatest elements seem straightforward to define.
>
I think the functions lub and glb could be used for this.
A path predicate would be existence of a chain of edges from one vertex to
> another.
>
Paths are already defined (see df-pths), but for undirected graphs only.
The definition of paths is based on the definition of walks, and the
definition of walks strongly depends on the property of a graph to be
undirected. Unfortunately, I see now way to provide a (usable) definition
for walks/trails/paths etc. which would work for directed as well as
undirected graphs.
Acyclic could be enforced by requiting that not vertex had a path to itself.
>
If there was a definition `DCycles` for cycles in directed graphs (as
provided by ~df-cycls for undirected graphs). this condition could be
expressed by using this definition, e.g., `( DCycles `` G ) = (/)`.
>
>
--
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/a7d57425-2dc0-467f-bd01-338cd873c703n%40googlegroups.com.
