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.

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) : (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.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

theorem SimpleGraph.Walk.IsHamiltonian.of_subsingleton {α : Type u_1} [DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b} [Subsingleton α] : p.IsHamiltonian

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 its vertex set must be finite.

theorem SimpleGraph.Walk.IsHamiltonian.support_toFinset {α : Type u_1} [DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b} [Fintype α] (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} [DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b} [Fintype α] (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.length_support {α : Type u_1} [DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b} [Fintype α] (hp : p.IsHamiltonian) : p.support.length = Fintype.card α

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) : Fin p.support.length ≃ α

If a path p is Hamiltonian, then p.support.get defines an equivalence between Fin p.support.length and α.

@[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✝ : α) : ↑(hp.supportGetEquiv.symm a✝) = List.idxOf a✝ p.support

@[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) : hp.supportGetEquiv i = p.support[↑i]

def SimpleGraph.Walk.IsHamiltonian.getVertEquiv {α : Type u_1} [DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b} (hp : p.IsHamiltonian) : Fin p.support.length ≃ α

If a path p is Hamiltonian, then p.getVert defines an equivalence between Fin p.support.length and α.

@[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) : hp.getVertEquiv a✝ = (p.getVert ∘ Fin.val) a✝

@[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✝ : α) : hp.getVertEquiv.symm a✝ = hp.supportGetEquiv.invFun a✝

theorem SimpleGraph.Walk.isHamiltonian_iff_support_get_bijective {α : Type u_1} [DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b} : p.IsHamiltonian ↔ Function.Bijective p.support.get

theorem SimpleGraph.Walk.IsHamiltonian.getVert_surjective {α : Type u_1} [DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b} (hp : p.IsHamiltonian) : Function.Surjective p.getVert

theorem SimpleGraph.Walk.isHamiltonian_iff_isPath_and_length_eq {α : Type u_1} [DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b} [Fintype α] : p.IsHamiltonian ↔ p.IsPath ∧ p.length = Fintype.card α - 1

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

A Hamiltonian cycle is a cycle that visits every vertex once.

• edges_nodup : p.edges.Nodup
• ne_nil : p ≠ nil
• support_nodup : p.support.tail.Nodup
• isHamiltonian_tail : 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) : (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 ↔ 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} [DecidableEq α] {G : SimpleGraph α} {a : α} {p : G.Walk a a} [Fintype α] (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

theorem SimpleGraph.Walk.isHamiltonianCycle_iff_isCycle_and_length_eq {α : Type u_1} [DecidableEq α] {G : SimpleGraph α} {a : α} {p : G.Walk a a} [Fintype α] : p.IsHamiltonianCycle ↔ p.IsCycle ∧ p.length = Fintype.card α

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

A Hamiltonian graph is a graph that contains a Hamiltonian cycle.

By convention, the singleton graph is considered to be Hamiltonian.

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

theorem SimpleGraph.not_isHamiltonian_of_isEmpty {α : Type u_1} [DecidableEq α] {G : SimpleGraph α} [Fintype α] [IsEmpty α] : ¬G.IsHamiltonian

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

theorem SimpleGraph.IsHamiltonian.of_card_eq_one {α : Type u_1} [DecidableEq α] {G : SimpleGraph α} [Fintype α] (h : Fintype.card α = 1) : G.IsHamiltonian

theorem SimpleGraph.not_isHamiltonian_of_card_eq_two {α : Type u_1} [DecidableEq α] {G : SimpleGraph α} [Fintype α] (h : Fintype.card α = 2) : ¬G.IsHamiltonian

@[simp]

theorem SimpleGraph.not_isHamiltonian_bot_of_card_ne_one {α : Type u_1} [DecidableEq α] [Fintype α] (h : Fintype.card α ≠ 1) : ¬⊥.IsHamiltonian

theorem SimpleGraph.IsHamiltonian.of_unique {α : Type u_1} [DecidableEq α] {G : SimpleGraph α} [Fintype α] [Unique α] : G.IsHamiltonian

theorem SimpleGraph.not_isHamiltonian_of_isBridge {V : Type u_3} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (h_order : 3 ≤ Fintype.card V) (e : Sym2 V) (he : G.IsBridge e) : ¬G.IsHamiltonian

A finite simple graph with at least three vertices and a bridge is not Hamiltonian.

More precisely, let G : SimpleGraph V be a simple graph on a finite vertex type V. If Fintype.card V ≥ 3 and there exists an edge of G which is a bridge, then G does not admit a Hamiltonian cycle, i.e. ¬ G.IsHamiltonian.