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/B33AF260-BB73-480C-A41B-EC49A0AD81EC%40gmx.net.
