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.
I'd also add existential uniqueness to disallow multiedges.
Least and greatest elements seem straightforward to define.
A path predicate would be existence of a chain of edges from one vertex to
another.
Acyclic could be enforced by requiting that not vertex had a path to itself.
--Brian
On Thursday, December 30, 2021 at 2:23:49 PM UTC-6 Alexander van der Vekens
wrote:
> Good hint, Thierry!
> But instead of mapping a Poset etc. as extensible structure to a graph,
> the extensible structure can be *made* a graph (that's because the
> structure is extensible!) by inserting an edge function into the slot
> ".ef", using the sSet operator. See, for example, ~structtousgr.
> As edge function, ( _I |` E ) could be chosen with E = { <. x, y >. | ( x
> ( le ‘ P ) y /\ -. E. z ( x ( le ‘ P ) z /\ z ( le ‘ P ) y ) ) } as
> proposed by Thierry.
>
> On Thursday, December 30, 2021 at 8:29:51 PM UTC+1 Thierry Arnoux wrote:
>
>> Posets, Tosets and Lattices are already defined in set.mm. I imagine one
>> may define a function F mapping them to their corresponding graphs :
>> vertices are the same base, edges are something like the set { <. x, y >. |
>> ( x ( le ‘ P ) y /\ -. E. z ( x ( le ‘ P ) z /\ z ( le ‘ P ) y ) ) }
>> Then, I think ran F would be the set of graphs you’re interested in.
>> BR,
>> _
>> Thierry
>>
>>
>>
--
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/d365c831-760d-41cf-aabe-d5db1783862en%40googlegroups.com.
