\begin{definition}[Definition:Edge Contraction]
Let $G$ be an undirected graph.
Let $e \in \map E G$ be an edge of $G$.
Then the '''graph obtained by contracting $e$ in $G$''', denoted by $G / e$, is the graph $H$ defined by:
:$\map V H = \paren {\map V G \setminus e} \cup \set v$
:$\map E H = \set {f \in \map E G: f \cap e = \O} \cup \set {u v: \exists f \in \map E G: u \in f \setminus e, f \cap e \ne \O}$
where $v \notin \map V G$ is a fresh object.
{{explain|A lot of the above - see talk page (in prep)}}
Informally, it is the graph obtained from $G$ by replacing the vertices incident to $e$ with a single vertex adjacent to all their neighbors.
\end{definition}