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) : Prop

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

theorem SimpleGraph.Walk.IsHamiltonian.map {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {G : SimpleGraph α} {a : α} {b : α} {p : G.Walk a b} {H : SimpleGraph β} (f : G →g H) (hf : Function.Bijective ⇑f) (hp : p.IsHamiltonian) : (SimpleGraph.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 : α) : c ∈ p.support

A hamiltonian path visits every vertex.

theorem SimpleGraph.Walk.IsHamiltonian.support_toFinset {α : Type u_1} [Fintype α] [DecidableEq α] {G : SimpleGraph α} {a : α} {b : α} {p : G.Walk a b} (hp : p.IsHamiltonian) : p.support.toFinset = Finset.univ

The support of a hamiltonian walk is the entire vertex set.

theorem SimpleGraph.Walk.IsHamiltonian.length_eq {α : Type u_1} [Fintype α] [DecidableEq α] {G : SimpleGraph α} {a : α} {b : α} {p : G.Walk a b} (hp : p.IsHamiltonian) : p.length = Fintype.card α - 1

The length of a hamiltonian path is one less than the number of vertices of the graph.

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) : p.IsHamiltonian

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) : p.IsHamiltonian ↔ ∀ (w : α), w ∈ p.support

structure SimpleGraph.Walk.IsHamiltonianCycle {α : Type u_1} [DecidableEq α] {G : SimpleGraph α} {a : α} (p : G.Walk a a) extends SimpleGraph.Walk.IsCycle : Prop

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

theorem SimpleGraph.Walk.IsHamiltonianCycle.isHamiltonian_tail {α : Type u_1} [DecidableEq α] {G : SimpleGraph α} {a : α} {p : G.Walk a a} (self : p.IsHamiltonianCycle) : (p.tail ⋯).IsHamiltonian

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} {β : Type u_2} [DecidableEq α] [DecidableEq β] {G : SimpleGraph α} {a : α} {p : G.Walk a a} {H : SimpleGraph β} (f : G →g H) (hf : Function.Bijective ⇑f) (hp : p.IsHamiltonianCycle) : (SimpleGraph.Walk.map f p).IsHamiltonianCycle

theorem SimpleGraph.Walk.isHamiltonianCycle_isCycle_and_isHamiltonian_tail {α : Type u_1} [DecidableEq α] {G : SimpleGraph α} {a : α} {p : G.Walk a a} : p.IsHamiltonianCycle ↔ ∃ (h : p.IsCycle), (p.tail ⋯).IsHamiltonian

theorem SimpleGraph.Walk.isHamiltonianCycle_iff_isCycle_and_support_count_tail_eq_one {α : Type u_1} [DecidableEq α] {G : SimpleGraph α} {a : α} {p : G.Walk a a} : p.IsHamiltonianCycle ↔ p.IsCycle ∧ ∀ (a_1 : α), List.count a_1 p.support.tail = 1

theorem SimpleGraph.Walk.IsHamiltonianCycle.mem_support {α : Type u_1} [DecidableEq α] {G : SimpleGraph α} {a : α} {p : G.Walk a a} (hp : p.IsHamiltonianCycle) (b : α) : b ∈ p.support

A hamiltonian cycle visits every vertex.

theorem SimpleGraph.Walk.IsHamiltonianCycle.length_eq {α : Type u_1} [Fintype α] [DecidableEq α] {G : SimpleGraph α} {a : α} {p : G.Walk a a} (hp : p.IsHamiltonianCycle) : p.length = Fintype.card α

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) : List.count a p.support = 2

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) : List.count b p.support = 1

def SimpleGraph.IsHamiltonian {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) : Prop

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)

theorem SimpleGraph.IsHamiltonian.mono {α : Type u_1} [Fintype α] [DecidableEq α] {G : SimpleGraph α} {H : SimpleGraph α} (hGH : G ≤ H) (hG : G.IsHamiltonian) : H.IsHamiltonian

theorem SimpleGraph.IsHamiltonian.connected {α : Type u_1} [Fintype α] [DecidableEq α] {G : SimpleGraph α} (hG : G.IsHamiltonian) : G.Connected