Trails and Eulerian trails #
This module contains additional theory about trails, including Eulerian trails (also known
as Eulerian circuits).
Main definitions #
The edges of a trail as a finset, since each edge in a trail appears exactly once.
An Eulerian trail (also known as an "Eulerian path") is a walk
p that visits every edge exactly once. The lemma
that these are trails.
p.is_circuit to get an Eulerian circuit (also known as an "Eulerian cycle").
The edge set of an Eulerian graph is finite.