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.
simple_graphis a structure for symmetric, irreflexive relations
setof vertices adjacent to a given vertex
finsetof vertices adjacent to a given vertex, if
A locally finite graph is one with instances
∀ v, fintype (G.neighbor_set v).
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
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).