Graph families and operations
Graph products, line graphs and other constructions, together with special families such as expanders and the hypercubic lattice.
DefinitionGraphs that are line graphs#✓fully proved
A simple graph \(G\) on a finite vertex type is a line graph if there are a natural number \(k\) and a simple graph \(H\) on the vertex set \(\{0, \dots, k-1\}\) such that \(G\) is isomorphic to the line graph \(L(H)\). Here \(L(H)\) has the edges of \(H\) as its vertices, and two distinct edges of \(H\) are adjacent in \(L(H)\) when they share an endpoint.
def SimpleGraph.IsLineGraph {V : Type*} [Fintype V] (G : SimpleGraph V) : Prop :=
∃ (k : ℕ) (H : SimpleGraph (Fin k)),
Nonempty (G ≃g H.lineGraph)DefinitionLexicographic product of graphs#✓fully proved
Given simple graphs \(X\) and \(Y\), the lexicographic product \(X[Y]\) of \(X\) and \(Y\) is the simple graph with vertex set \(V(X) \times V(Y)\) in which two vertices \((x_1, y_1)\) and \((x_2, y_2)\) are adjacent exactly when \(x_1\) and \(x_2\) are adjacent in \(X\), or \(x_1 = x_2\) and \(y_1\) and \(y_2\) are adjacent in \(Y\).
def _root_.SimpleGraph.lexProduct {V W : Type*} (G : SimpleGraph V) (H : SimpleGraph W) :
SimpleGraph (V × W) :=
SimpleGraph.fromRel fun (p q : V × W) => G.Adj p.1 q.1 ∨ p.1 = q.1 ∧ H.Adj p.2 q.2Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.