Metamath Proof Explorer


Table of Contents - 16.1. Vertices and edges

In the following, the vertices and (indexed) edges for an arbitrary class (called "graph" in the following) are defined and examined. The main result of this section is to show that the set of vertices of a graph is the first component of the graph if it is represented by an ordered pair (see opvtxfv), or the base set of the graph if it is represented as extensible structure (see basvtxval), and that the set of indexed edges resp. the edge function is the second component of the graph if it is represented by an ordered pair (see opiedgfv), or the component of the graph if it is represented as extensible structure (see edgfiedgval). Finally, it is shown that the set of edges of a graph is the range of its edge function: , see edgval.

Usually, a graph is a set. If is a proper class, however, it represents the null graph (without vertices and edges), because and holds, see vtxvalprc and iedgvalprc.

Up to the end of this section, the edges need not be related to the vertices. Once undirected hypergraphs are defined (see df-uhgr), the edges become nonempty sets of vertices, and by this obtain their meaning as "connectors" of vertices.

  1. The edge function extractor for extensible structures
    1. cedgf
    2. df-edgf
    3. edgfid
    4. edgfndxnn
    5. edgfndxid
    6. baseltedgf
    7. slotsbaseefdif
  2. Vertices and indexed edges
    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
  3. Edges as range of the edge function
    1. cedg
    2. df-edg
    3. edgval
    4. iedgedg
    5. edgopval
    6. edgov
    7. edgstruct
    8. edgiedgb
    9. edg0iedg0