Documentation

Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Hamiltonian Graphs #

In this file we introduce hamiltonian paths, cycles and graphs.

Main definitions #

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} {β : 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.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.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.

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

    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
      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 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

      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)
      Instances For
        theorem SimpleGraph.IsHamiltonian.mono {α : Type u_1} [DecidableEq α] {G : SimpleGraph α} [Fintype α] {H : SimpleGraph α} (hGH : G H) (hG : G.IsHamiltonian) :
        H.IsHamiltonian
        theorem SimpleGraph.IsHamiltonian.connected {α : Type u_1} [DecidableEq α] {G : SimpleGraph α} [Fintype α] (hG : G.IsHamiltonian) :
        G.Connected