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/162dee32-1e42-4705-be95-ecfe36420442n%40googlegroups.com.
