Hamiltonian Graphs #
In this file we introduce hamiltonian paths, cycles and graphs.
Main definitions #
SimpleGraph.Walk.IsHamiltonian
: Predicate for a walk to be hamiltonian.SimpleGraph.Walk.IsHamiltonianCycle
: Predicate for a walk to be a hamiltonian cycle.SimpleGraph.IsHamiltonian
: Predicate for a graph to be hamiltonian.
A hamiltonian path is a walk p
that visits every vertex exactly once. Note that while
this definition doesn't contain that p
is a path, p.isPath
gives that.
Equations
- p.IsHamiltonian = ∀ (a_1 : α), List.count a_1 p.support = 1
Instances For
A hamiltonian path visits every vertex.
Hamiltonian paths are paths.
A path whose support contains every vertex is hamiltonian.
The support of a hamiltonian walk is the entire vertex set.
The length of a hamiltonian path is one less than the number of vertices of the graph.
A hamiltonian cycle is a cycle that visits every vertex once.
- edges_nodup : p.edges.Nodup
- ne_nil : p ≠ SimpleGraph.Walk.nil
- support_nodup : p.support.tail.Nodup
- isHamiltonian_tail : p.tail.IsHamiltonian
Instances For
A hamiltonian cycle visits every vertex.
The length of a hamiltonian cycle is the number of vertices.
A hamiltonian graph is a graph that contains a hamiltonian cycle.
By convention, the singleton graph is considered to be hamiltonian.
Equations
- G.IsHamiltonian = (Fintype.card α ≠ 1 → ∃ (a : α) (p : G.Walk a a), p.IsHamiltonianCycle)