Simple graphs #
This module defines simple graphs on a vertex type
V as an
irreflexive symmetric relation.
There is a basic API for locally finite graphs and for graphs with finitely many vertices.
Main definitions #
simple_graphis a structure for symmetric, irreflexive relations
setof vertices adjacent to a given vertex
finsetof vertices adjacent to a given vertex, if
setof edges containing a given vertex
finsetof edges containing a given vertex, if
Implementation notes #
A locally finite graph is one with instances
∀ v, fintype (G.neighbor_set v).
Naming Conventions #
- If the vertex type of a graph is finite, we refer to its cardinality as
TODO: This is the simplest notion of an unoriented graph. This should eventually fit into a more complete combinatorics hierarchy which includes multigraphs and directed graphs. We begin with simple graphs in order to start learning what the combinatorics hierarchy should look like.
TODO: Part of this would include defining, for example, subgraphs of a simple graph.
A simple graph is an irreflexive symmetric relation
adj on a vertex type
The relation describes which pairs of vertices are adjacent.
There is exactly one edge for every pair of adjacent edges;
simple_graph.edge_set for the corresponding edge set.
Two vertices are adjacent iff there is an edge between them. The
v ≠ w ensures they are different endpoints of the edge,
which is necessary since when
v = w the existential
∃ (e ∈ G.edge_set), v ∈ e ∧ w ∈ e is satisfied by every edge
There is an equivalence between the set of edges incident to a given vertex and the set of vertices adjacent to the vertex.
Finiteness at a vertex #
This section contains definitions and lemmas concerning vertices that
have finitely many adjacent vertices. We denote this condition by
fintype (G.neighbor_set v).
If the condition
G.adj v w fails, then
the best we can do in general.
Complement of a simple graph #
This section contains definitions and lemmas concerning the complement of a simple graph.
compl G to be the
simple_graph V such that no two adjacent vertices in
are adjacent in the complement, and every nonadjacent pair of vertices is adjacent
(still ensuring that vertices are not adjacent to themselves.)