Lax Lean Archive

Hamiltonian cycles

Lax881656.HamiltonianCycle · concepts/Lax881656/HamiltonianCycle.lean · lax-881656

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    A Hamiltonian cycle in a graph is a cycle that visits every vertex. A graph has a Hamiltonian cycle when such a closed walk exists.

    Concept map
    1 concept; 1 descendant hidden
    100%
    Open claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Paths
    2
    3/-!
    4---
    5title: Hamiltonian cycles
    6type: definition
    7---
    8A Hamiltonian cycle in a graph is a cycle that visits every vertex. A graph
    9has a Hamiltonian cycle when such a closed walk exists.
    10
    11# Formalization notes
    12
    13A cycle is represented by mathlib's closed-walk predicate, which ensures that
    14no vertex is repeated except for the common start and end. The separate
    15spanning condition says that every graph vertex belongs to its support.
    16-/
    17
    18set_option autoImplicit false
    19
    20namespace Lax881656.HamiltonianCycle
    21
    22/-- A closed walk is a Hamiltonian cycle when it is a cycle and visits every
    23vertex of the graph. -/
    24def IsHamiltonianCycle {V : Type*} [DecidableEq V] {G : SimpleGraph V}
    25 {v : V} (cycle : G.Walk v v) : Prop :=
    26 cycle.IsCycle ∧ ∀ w : V, w ∈ cycle.support
    27
    28/-- A graph has a Hamiltonian cycle when it contains a spanning cycle. -/
    29def HasHamiltonianCycle {V : Type*} [DecidableEq V]
    30 (G : SimpleGraph V) : Prop :=
    31 ∃ v : V, ∃ cycle : G.Walk v v, IsHamiltonianCycle cycle
    32
    33end Lax881656.HamiltonianCycle
    34
    Formalization notes

    A cycle is represented by mathlib's closed-walk predicate, which ensures that no vertex is repeated except for the common start and end. The separate spanning condition says that every graph vertex belongs to its support.

    Builds on

    none

    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…