Cycle lengths and circumference

DefinitionCycle lengths#✓fully proved

For a simple graph \(G\), the set of cycle lengths of \(G\) is the set of natural numbers \(m\) such that \(G\) contains a cycle of length \(m\).

def cycleLengths {α : Type*} (G : SimpleGraph α) : Set ℕ :=
  {m | ∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ w.length = m}

Used by 3

Used byErdős Problem 751 · Statement of Erdős Problem 63 · Odd cycle lengths

DefinitionOdd cycle lengths#✓fully proved

For a simple graph \(G\), the set of odd cycle lengths of \(G\) is the set of those cycle lengths of \(G\) that are odd, that is, the odd natural numbers \(m\) such that \(G\) contains a cycle of length \(m\).

def oddCycleLengths {α : Type*} (G : SimpleGraph α) : Set ℕ :=
  {m ∈ G.cycleLengths | Odd m}

Uses 1 · Used by 1

Statement usesCycle lengths

Used byOdd cycle lengths and infinite chromatic number (Erdős Problem 57)

DefinitionLongest cycle in a graph#✓fully proved

A cycle is globally longest if no cycle in the graph has more edges.

public def IsLongestCycle {V : Type*} {G : SimpleGraph V} {v : V}
    (p : G.Walk v v) : Prop :=
  p.IsCycle ∧ ∀ (w : V) (q : G.Walk w w), q.IsCycle → q.length ≤ p.length

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.