> On Jun 5, 2021, at 8:31 AM, 'Alexander van der Vekens' via Metamath
> <[email protected]> wrote:
>
> In October 2020, I started the revision of the definitions and theorems for
> Graph Theory (PART 16 of set.mm), based on the discussion in Github issue
> #1418:
>
> Since the beginning of dealing with graph theory in set.mm, the question if
> graphs shall be represented as ordered pairs (of a set of vertices and a set
> of edges) or as extensible structures (the set of vertices as base set, and a
> special slot for the edges) was open (the current graph theory in PART 16 is
> based on the representation by ordered pairs).
>
> The new approach is based on the definitions ~df-vtx and ~df-iedg for
> functions Vtx and iEdg to get the vertices and (indexed) edges of graphs
> represented by an arbitrary class G, and this works for G being either an
> ordered pair or an extensible structure (and some other, maybe degenerated
> cases). If required, other representations could be supported by extending
> the two definitions in the future (with no changes of the other definitions
> and theorems!). The revised graph theory is build on these two functions
> (usually setting V = ( Vtx ` G )and E = ( iEdg ` G ) and using V and E in the
> definitions and theorems only), disregarding the concrete representation of a
> graph. Therefore, a decision how to represent a graph will be not necessary
> anymore.
It all makes sense to me. I think it’s important that this explanation be in
set.mm itself, either as part of the new PART 16 header description, or as part
of a key definition (like df-vtx). A brief description on “why is this
representation being used” would help people understand it.
--- David A. Wheeler
--
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/65E05642-A800-4DAF-A859-19C5F65AB921%40dwheeler.com.
