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.
def
SimpleGraph.Walk.IsHamiltonian
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a b : α}
(p : G.Walk a b)
:
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
theorem
SimpleGraph.Walk.IsHamiltonian.map
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{β : Type u_2}
[DecidableEq β]
{H : SimpleGraph β}
{a b : α}
{p : G.Walk a b}
(f : G →g H)
(hf : Function.Bijective ⇑f)
(hp : p.IsHamiltonian)
:
(Walk.map f p).IsHamiltonian
@[simp]
theorem
SimpleGraph.Walk.IsHamiltonian.mem_support
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a b : α}
{p : G.Walk a b}
(hp : p.IsHamiltonian)
(c : α)
:
A Hamiltonian path visits every vertex.
theorem
SimpleGraph.Walk.IsHamiltonian.isPath
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a b : α}
{p : G.Walk a b}
(hp : p.IsHamiltonian)
:
p.IsPath
Hamiltonian paths are paths.
theorem
SimpleGraph.Walk.IsPath.isHamiltonian_of_mem
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a b : α}
{p : G.Walk a b}
(hp : p.IsPath)
(hp' : ∀ (w : α), w ∈ p.support)
:
A path whose support contains every vertex is Hamiltonian.
theorem
SimpleGraph.Walk.IsPath.isHamiltonian_iff
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a b : α}
{p : G.Walk a b}
(hp : p.IsPath)
:
theorem
SimpleGraph.Walk.IsHamiltonian.of_subsingleton
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a b : α}
{p : G.Walk a b}
[Subsingleton α]
:
@[implicit_reducible]
def
SimpleGraph.Walk.IsHamiltonian.fintype
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a b : α}
{p : G.Walk a b}
(hp : p.IsHamiltonian)
:
Fintype α
If a path p is Hamiltonian then the graph has finitely many vertices.
Instances For
theorem
SimpleGraph.Walk.IsHamiltonian.finite
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a b : α}
{p : G.Walk a b}
(hp : p.IsHamiltonian)
:
Finite α
If a path p is Hamiltonian then the graph has finitely many vertices.
@[simp]
theorem
SimpleGraph.Walk.not_isHamiltonian_of_infinite
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a b : α}
{p : G.Walk a b}
[h : Infinite α]
:
theorem
SimpleGraph.Walk.IsHamiltonian.toFinset_support
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a b : α}
{p : G.Walk a b}
[Fintype α]
(hp : p.IsHamiltonian)
:
The support of a Hamiltonian walk is the entire vertex set.
@[deprecated SimpleGraph.Walk.IsHamiltonian.toFinset_support (since := "2026-03-11")]
theorem
SimpleGraph.Walk.IsHamiltonian.support_toFinset
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a b : α}
{p : G.Walk a b}
[Fintype α]
(hp : p.IsHamiltonian)
:
Alias of SimpleGraph.Walk.IsHamiltonian.toFinset_support.
The support of a Hamiltonian walk is the entire vertex set.
theorem
SimpleGraph.Walk.IsHamiltonian.setOf_support
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a b : α}
{p : G.Walk a b}
(hp : p.IsHamiltonian)
:
theorem
SimpleGraph.Walk.IsHamiltonian.length_eq
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a b : α}
{p : G.Walk a b}
[Fintype α]
(hp : p.IsHamiltonian)
:
The length of a Hamiltonian path is one less than the number of vertices of the graph.
theorem
SimpleGraph.Walk.IsHamiltonian.length_support
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a b : α}
{p : G.Walk a b}
[Fintype α]
(hp : p.IsHamiltonian)
:
The length of the support of a Hamiltonian path equals the number of vertices of the graph.
def
SimpleGraph.Walk.IsHamiltonian.supportGetEquiv
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a b : α}
{p : G.Walk a b}
(hp : p.IsHamiltonian)
:
If a path p is Hamiltonian, then p.support.get defines an equivalence between
Fin p.support.length and α.
Equations
Instances For
@[simp]
theorem
SimpleGraph.Walk.IsHamiltonian.supportGetEquiv_symm_apply_val
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a b : α}
{p : G.Walk a b}
(hp : p.IsHamiltonian)
(a✝ : α)
:
@[simp]
theorem
SimpleGraph.Walk.IsHamiltonian.supportGetEquiv_apply
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a b : α}
{p : G.Walk a b}
(hp : p.IsHamiltonian)
(i : Fin p.support.length)
:
def
SimpleGraph.Walk.IsHamiltonian.getVertEquiv
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a b : α}
{p : G.Walk a b}
(hp : p.IsHamiltonian)
:
If a path p is Hamiltonian, then p.getVert defines an equivalence between
Fin p.support.length and α.
Equations
- hp.getVertEquiv = { toFun := p.getVert ∘ Fin.val, invFun := hp.supportGetEquiv.invFun, left_inv := ⋯, right_inv := ⋯ }
Instances For
@[simp]
theorem
SimpleGraph.Walk.IsHamiltonian.getVertEquiv_apply
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a b : α}
{p : G.Walk a b}
(hp : p.IsHamiltonian)
(a✝ : Fin p.support.length)
:
@[simp]
theorem
SimpleGraph.Walk.IsHamiltonian.getVertEquiv_symm_apply
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a b : α}
{p : G.Walk a b}
(hp : p.IsHamiltonian)
(a✝ : α)
:
theorem
SimpleGraph.Walk.isHamiltonian_iff_support_get_bijective
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a b : α}
{p : G.Walk a b}
:
theorem
SimpleGraph.Walk.IsHamiltonian.getVert_surjective
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a b : α}
{p : G.Walk a b}
(hp : p.IsHamiltonian)
:
theorem
SimpleGraph.Walk.IsHamiltonian.injective_of_isPath_map
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{β : Type u_2}
{H : SimpleGraph β}
{a b : α}
{p : G.Walk a b}
{f : G →g H}
(hp : p.IsHamiltonian)
(h : (Walk.map f p).IsPath)
:
theorem
SimpleGraph.Walk.isHamiltonian_iff_isPath_and_length_eq
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a b : α}
{p : G.Walk a b}
[Fintype α]
:
structure
SimpleGraph.Walk.IsHamiltonianCycle
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a : α}
(p : G.Walk a a)
extends p.IsCycle :
A Hamiltonian cycle is a cycle that visits every vertex once.
- edges_nodup : p.edges.Nodup
- isHamiltonian_tail : p.tail.IsHamiltonian
Instances For
theorem
SimpleGraph.Walk.IsHamiltonianCycle.isCycle
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a : α}
{p : G.Walk a a}
(hp : p.IsHamiltonianCycle)
:
p.IsCycle
theorem
SimpleGraph.Walk.IsHamiltonianCycle.map
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{β : Type u_2}
[DecidableEq β]
{H : SimpleGraph β}
{a : α}
{f : G →g H}
{p : G.Walk a a}
(hf : Function.Bijective ⇑f)
(hp : p.IsHamiltonianCycle)
:
(Walk.map f p).IsHamiltonianCycle
theorem
SimpleGraph.Walk.IsHamiltonianCycle.finite
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a : α}
{p : G.Walk a a}
(hp : p.IsHamiltonianCycle)
:
Finite α
If a cycle p is Hamiltonian then the graph has finitely many vertices.
@[simp]
theorem
SimpleGraph.Walk.not_isHamiltonianCycle_of_infinite
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a : α}
{p : G.Walk a a}
[h : Infinite α]
:
theorem
SimpleGraph.Walk.isHamiltonianCycle_isCycle_and_isHamiltonian_tail
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a : α}
{p : G.Walk a a}
:
theorem
SimpleGraph.Walk.isHamiltonianCycle_iff_isCycle_and_support_count_tail_eq_one
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a : α}
{p : G.Walk a a}
:
theorem
SimpleGraph.Walk.IsHamiltonianCycle.mem_support
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a : α}
{p : G.Walk a a}
(hp : p.IsHamiltonianCycle)
(b : α)
:
A Hamiltonian cycle visits every vertex.
theorem
SimpleGraph.Walk.IsHamiltonianCycle.length_eq
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a : α}
{p : G.Walk a a}
[Fintype α]
(hp : p.IsHamiltonianCycle)
:
The length of a Hamiltonian cycle is the number of vertices.
theorem
SimpleGraph.Walk.IsHamiltonianCycle.count_support_self
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a : α}
{p : G.Walk a a}
(hp : p.IsHamiltonianCycle)
:
theorem
SimpleGraph.Walk.IsHamiltonianCycle.support_count_of_ne
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a b : α}
{p : G.Walk a a}
(hp : p.IsHamiltonianCycle)
(h : a ≠ b)
:
theorem
SimpleGraph.Walk.isHamiltonianCycle_iff_isCycle_and_length_eq
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a : α}
{p : G.Walk a a}
[Fintype α]
:
@[simp]
theorem
SimpleGraph.Walk.isHamiltonianCycle_rotate
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a v : α}
{p : G.Walk a a}
(hv : v ∈ p.support)
:
theorem
SimpleGraph.Walk.IsHamiltonianCycle.of_rotate
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a v : α}
{p : G.Walk a a}
(hv : v ∈ p.support)
:
(p.rotate v hv).IsHamiltonianCycle → p.IsHamiltonianCycle
Alias of the forward direction of SimpleGraph.Walk.isHamiltonianCycle_rotate.
theorem
SimpleGraph.Walk.IsHamiltonianCycle.rotate
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
{a v : α}
{p : G.Walk a a}
(hv : v ∈ p.support)
:
p.IsHamiltonianCycle → (p.rotate v hv).IsHamiltonianCycle
Alias of the reverse direction of SimpleGraph.Walk.isHamiltonianCycle_rotate.
A Hamiltonian graph is a graph that contains a Hamiltonian cycle.
This is equivalent to there being an Hamiltonian cycle based at each vertex.
See IsHamiltonian.exists_isHamiltonianCycle.
By convention, the singleton graph is considered to be Hamiltonian and the empty graph is not.
Equations
- G.IsHamiltonian = (Fintype.card α ≠ 1 → ∃ (a : α) (p : G.Walk a a), p.IsHamiltonianCycle)
Instances For
theorem
SimpleGraph.IsHamiltonian.exists_isHamiltonianCycle
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
[Fintype α]
[Nontrivial α]
(hG : G.IsHamiltonian)
(v : α)
:
∃ (p : G.Walk v v), p.IsHamiltonianCycle
theorem
SimpleGraph.IsHamiltonian.mono
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
[Fintype α]
{H : SimpleGraph α}
(hGH : G ≤ H)
(hG : G.IsHamiltonian)
:
theorem
SimpleGraph.not_isHamiltonian_of_isEmpty
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
[Fintype α]
[IsEmpty α]
:
theorem
SimpleGraph.IsHamiltonian.connected
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
[Fintype α]
(hG : G.IsHamiltonian)
:
theorem
SimpleGraph.IsHamiltonian.of_card_eq_one
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
[Fintype α]
(h : Fintype.card α = 1)
:
theorem
SimpleGraph.not_isHamiltonian_of_card_eq_two
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
[Fintype α]
(h : Fintype.card α = 2)
:
@[simp]
theorem
SimpleGraph.not_isHamiltonian_bot_of_card_ne_one
{α : Type u_1}
[DecidableEq α]
[Fintype α]
(h : Fintype.card α ≠ 1)
:
theorem
SimpleGraph.IsHamiltonian.of_unique
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
[Fintype α]
[Unique α]
:
theorem
SimpleGraph.IsBridge.not_isHamiltonian
{α : Type u_1}
[DecidableEq α]
{G : SimpleGraph α}
[Fintype α]
{e : Sym2 α}
(he : G.IsBridge e)
:
A finite simple graph with a bridge is not hamiltonian.