Říha's cycle lemma

DefinitionBound vertices of a closed walk#✓fully proved

Let \(c\) be a closed walk in a simple graph \(G\). A vertex \(y\) is bound to \(c\) when \(y\) lies on \(c\) and every neighbor of \(y\) in \(G\) lies on \(c\).

public def Walk.IsBoundVertex {V : Type*} {G : SimpleGraph V} {x : V}
    (c : G.Walk x x) (y : V) : Prop :=
  y ∈ c.support ∧ ∀ ⦃z⦄, G.Adj y z → z ∈ c.support

Used by 3

Used byStrengthened Fleischner theorem · Říha's cycle lemma · Characterization of bound vertices

TheoremCharacterization of bound vertices#✓fully proved

Let \(c\) be a closed walk in a simple graph \(G\). A vertex \(y\) is bound to \(c\) if and only if \(y\) lies on \(c\) and every neighbor of \(y\) in \(G\) lies on \(c\).

public theorem Walk.isBoundVertex_iff {V : Type*} {G : SimpleGraph V} {x : V}
    (c : G.Walk x x) (y : V) :
    c.IsBoundVertex y ↔ y ∈ c.support ∧ ∀ ⦃z⦄, G.Adj y z → z ∈ c.support

Uses 1

Statement usesBound vertices of a closed walk

TheoremŘíha's cycle lemma#✓fully proved

Let \(G\) be a finite \(2\)-vertex-connected simple graph. Then for every vertex \(x\) of \(G\) there is a cycle \(c\) through \(x\) and a vertex \(y \ne x\) that is bound to \(c\): \(y\) lies on \(c\) and every neighbor of \(y\) in \(G\) lies on \(c\).

public theorem IsVertexConnected.exists_cycle_bound_vertex
    {V : Type*} [Fintype V] {G : SimpleGraph V} (hG : G.IsVertexConnected 2) (x : V) :
    ∃ c : G.Walk x x, c.IsCycle ∧ ∃ y, y ≠ x ∧ c.IsBoundVertex y

Uses 5 · Used by 1

Statement uses\(k\)-vertex-connected graph · Bound vertices of a closed walk

Proof usesA \(k\)-vertex-connected graph with \(k \ge 1\) is connected · Deleting one vertex from a \(k\)-vertex-connected graph with \(k \ge 2\) · Cycles through each vertex of a 2-vertex-connected graph

Used byStrengthened Fleischner theorem

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.