# Metamath Proof Explorer

The key concepts in graph theory are vertices and edges. In general, a graph "consists" (at least) of two sets: the set of vertices and the set of edges. The edges "connect" vertices. The meaning of "connect" is different for different kinds of graphs (directed/undirected graphs, hyper-/pseudo-/ multi-/simple graphs, etc.). The simplest way to represent a graph (of any kind) is to define a graph as "an ordered pair of disjoint sets (V, E)" (see section I.1 in [Bollobas] p. 1), or in the notation of Metamath: .

Another way is to regard a graph as a mathematical structure, which consistes at least of a set (of vertices) and a relation between the vertices (edge function), but which can be enhanced by additional features (see Wikipedia "Mathematical structure", 24-Sep-2020, https://en.wikipedia.org/wiki/Mathematical_structure): "In mathematics, a structure is a set endowed with some additional features on the set (e.g., operation, relation, metric, topology). Often, the additional features are attached or related to the set, so as to provide it with some additional meaning or significance.". Such structures are provided as "extensible structures" in Metamath, see df-struct.

To allow for expressing and proving most of the theorems for graphs independently from their representation, the functions and are defined (see df-vtx and df-iedg), which provide the vertices resp. (indexed) edges of an arbitrary class which represents a graph: resp. . In literature, these functions are often denoted also by "V" and "E", see section I.1 in [Bollobas] p. 1 ("If G is a graph, then V = V(G) is the vertex set of G, and E = E(G) is the edge set.") or section 1.1 in [Diestel] p. 2 ("The vertex set of graph G is referred to as V(G), its edge set as E(G).").

Instead of providing edges themselves, is intended to provide a function as mapping of "indices" (the domain of the function) to the edges (therefore called "set of indexed edges"), which allows for hyper-/pseudo-/multigraphs with more than one edge between two (or more) vertices. For example, e1 = e(1) = { a, b } and e2 = e(2) = { a, b } are two different edges connecting the same two vertices a and b (in a pseudograph). In section 1.10 of [Diestel] p. 28, the edge function is defined differently: as "map E -> V u. [V]^2 assigning to every edge either one or two vertices, its end.". Here, the domain is the set of abstract edges: for two different edges e1 and e2 connecting the same two vertices a and b, we would have e(e1) = e(e2) = { a, b }. Since the set of abstract edges can be chosen as index set, these definitions are equivalent.

The result of these functions are as expected: for a graph represented as ordered pair (), the set of vertices is (see opvtxval) and the set of (indexed) edges is (see opiedgval), or if is given as ordered pair , the set of vertices is (see opvtxfv) and the set of (indexed) edges is (see opiedgfv).

And for a graph represented as extensible structure (), the set of vertices is (see funvtxval) and the set of (indexed) edges is (see funiedgval), or if is given in its simplest form as extensible structure with two slots (), the set of vertices is (see struct2grvtx) and the set of (indexed) edges is (see struct2griedg).

These two representations are convertible, see graop and grastruct: If is a graph (for example ), then represents essentially the same graph, and if is a graph (for example ), then represents essentially the same graph. In both cases, and hold. Theorems gropd and gropeld show that if any representation of a graph with vertices and edges has a certain property, then the ordered pair of the set of vertices and the set of edges (which is such a representation of a graph with vertices and edges ) has this property. Analogously, theorems grstructd and grstructeld show that if any representation of a graph with vertices and edges has a certain property, then any extensible structure with base set and value in the slot for edge functions (which is also such a representation of a graph with vertices and edges ) has this property.

Besides the usual way to represent graphs without edges (consisting of unconnected vertices only), which would be or , a structure without a slot for edges can be used: , see snstrvtxval and snstriedgval. Analogously, the empty set can be used to represent the null graph, see vtxval0 and iedgval0, which can also be represented by or . Even proper classes can be used to represent the null graph, see vtxvalprc and iedgvalprc.

Other classes should not be used to represent graphs, because there could be a degenerate behavior of the vertex set and (indexed) edge functions, see vtxvalsnop resp. iedgvalsnop, and vtxval3sn resp. iedgval3sn. Avoid directly depending on this detail so that theorems will not depend on the Kuratowski construction of ordered pairs, see also the comment for df-op.

1. Definitions and basic properties
2. The vertices and edges of a graph represented as ordered pair
3. The vertices and edges of a graph represented as extensible structure
4. Representations of graphs without edges
5. Degenerated cases of representations of graphs