Fleischner's theorem

DefinitionCollapsing the complement of a set#✓fully proved

For a set \(D \subseteq V\), the collapse map sends \(V\) to \(D\) together with one new vertex, the contraction vertex: each \(v \in D\) is sent to itself, and each \(v \notin D\) is sent to the contraction vertex.

public noncomputable def collapseOutside {V : Type*} (D : Set V) : V → Option D := by
  classical
  exact fun v ↦ if hv : v ∈ D then some ⟨v, hv⟩ else none

Used by 9

Used byPreimage of the contraction vertex under the collapse map · Preimages of retained vertices under the collapse map · The collapse map fixes the retained set · The collapse map sends the complement to the contraction vertex · The collapse map is surjective · Contracting the complement of a vertex set · Contracting the complement preserves 2-connectivity · Neighbors of the contraction vertex · Contraction preserves adjacency among retained vertices

TheoremThe collapse map fixes the retained set#✓fully proved

For a set \(D \subseteq V\), the collapse map from \(V\) to \(D\) together with the contraction vertex sends each \(v \in D\) to \(v\) itself.

@[simp]
public theorem collapseOutside_of_mem {V : Type*} (D : Set V) {v : V} (hv : v ∈ D) :
    collapseOutside D v = some ⟨v, hv⟩

Uses 1 · Used by 6

Statement usesCollapsing the complement of a set

Used byPreimage of the contraction vertex under the collapse map · Preimages of retained vertices under the collapse map · The collapse map is surjective · Contracting the complement preserves 2-connectivity · Neighbors of the contraction vertex · Contraction preserves adjacency among retained vertices

TheoremThe collapse map sends the complement to the contraction vertex#✓fully proved

For a set \(D \subseteq V\), the collapse map from \(V\) to \(D\) together with the contraction vertex sends each vertex \(v \notin D\) to the contraction vertex.

@[simp]
public theorem collapseOutside_of_notMem {V : Type*} (D : Set V) {v : V} (hv : v ∉ D) :
    collapseOutside D v = none

Uses 1 · Used by 5

Statement usesCollapsing the complement of a set

Used byPreimage of the contraction vertex under the collapse map · Preimages of retained vertices under the collapse map · The collapse map is surjective · Contracting the complement preserves 2-connectivity · Neighbors of the contraction vertex

TheoremPreimages of retained vertices under the collapse map#✓fully proved

For a set \(D \subseteq V\), a vertex \(v \in V\) and an element \(a \in D\), the collapse map from \(V\) to \(D\) together with the contraction vertex sends \(v\) to \(a\) if and only if \(v = a\).

@[simp]
public theorem collapseOutside_eq_some_iff {V : Type*} (D : Set V) (v : V) (a : D) :
    collapseOutside D v = some a ↔ v = a

Uses 3 · Used by 3

Statement usesCollapsing the complement of a set

Proof usesThe collapse map fixes the retained set · The collapse map sends the complement to the contraction vertex

Used byContracting the complement preserves 2-connectivity · Neighbors of the contraction vertex · Contraction preserves adjacency among retained vertices

TheoremPreimage of the contraction vertex under the collapse map#✓fully proved

For a set \(D \subseteq V\) and a vertex \(v \in V\), the collapse map from \(V\) to \(D\) together with the contraction vertex sends \(v\) to the contraction vertex if and only if \(v \notin D\).

@[simp]
public theorem collapseOutside_eq_none_iff {V : Type*} (D : Set V) (v : V) :
    collapseOutside D v = none ↔ v ∉ D

Uses 3 · Used by 1

Statement usesCollapsing the complement of a set

Proof usesThe collapse map fixes the retained set · The collapse map sends the complement to the contraction vertex

Used byNeighbors of the contraction vertex

TheoremThe collapse map is surjective#✓fully proved

For a set \(D \subseteq V\) whose complement \(V \setminus D\) is nonempty, the collapse map from \(V\) to \(D\) together with the contraction vertex is surjective.

public theorem collapseOutside_surjective {V : Type*} {D : Set V} (hD : Dᶜ.Nonempty) :
    Function.Surjective (collapseOutside D)

Uses 3 · Used by 1

Statement usesCollapsing the complement of a set

Proof usesThe collapse map fixes the retained set · The collapse map sends the complement to the contraction vertex

Used byContracting the complement preserves 2-connectivity

DefinitionContracting the complement of a vertex set#✓fully proved

Let \(G\) be a simple graph on a vertex set \(V\) and let \(D \subseteq V\). Contracting the complement of \(D\) to a single vertex gives the simple graph whose vertices are the elements of \(D\) together with one new vertex \(\ast\), in which two vertices \(a, b \in D\) are adjacent exactly when they are adjacent in \(G\), and a vertex \(a \in D\) is adjacent to \(\ast\) exactly when \(a\) has a neighbour in \(G\) outside \(D\). The new vertex \(\ast\) is present even when \(D = V\), and is then isolated.

public noncomputable def contractOutside {V : Type*} (G : SimpleGraph V) (D : Set V) :
    SimpleGraph (Option D) :=
  G.map (collapseOutside D)

Uses 1 · Used by 4

Statement usesCollapsing the complement of a set

Used byContracting the complement preserves 2-connectivity · Neighbors of the contraction vertex · Contraction preserves adjacency among retained vertices · Strengthened Fleischner theorem

TheoremContraction preserves adjacency among retained vertices#✓fully proved

Let \(G\) be a graph on \(V\), let \(D \subseteq V\), and contract \(V \setminus D\) to a single vertex. Two vertices \(a, b \in D\) are adjacent in the contracted graph if and only if they are adjacent in \(G\).

@[simp]
public theorem contractOutside_adj_some {V : Type*} (G : SimpleGraph V) (D : Set V)
    (a b : D) :
    (G.contractOutside D).Adj (some a) (some b) ↔ G.Adj a b

Uses 4 · Used by 2

Statement usesContracting the complement of a vertex set

Proof usesCollapsing the complement of a set · Preimages of retained vertices under the collapse map · The collapse map fixes the retained set

Used byContracting the complement preserves 2-connectivity · Strengthened Fleischner theorem

TheoremNeighbors of the contraction vertex#✓fully proved

Let \(G\) be a graph on \(V\), let \(D \subseteq V\), and contract \(V \setminus D\) to a single vertex. A vertex \(a \in D\) is adjacent to the contraction vertex in the contracted graph if and only if \(a\) is adjacent in \(G\) to some vertex \(v \notin D\).

@[simp]
public theorem contractOutside_adj_none {V : Type*} (G : SimpleGraph V) (D : Set V)
    (a : D) :
    (G.contractOutside D).Adj (some a) none ↔ ∃ v ∉ D, G.Adj a v

Uses 6 · Used by 1

Statement usesContracting the complement of a vertex set

Proof usesCollapsing the complement of a set · Preimage of the contraction vertex under the collapse map · Preimages of retained vertices under the collapse map · The collapse map fixes the retained set · The collapse map sends the complement to the contraction vertex

Used byStrengthened Fleischner theorem

TheoremContracting the complement preserves 2-connectivity#✓fully proved

Let \(G\) be a 2-vertex-connected graph on a finite vertex set \(V\), and let \(D \subseteq V\) be a set with at least two elements that induces a connected subgraph of \(G\) and whose complement \(V \setminus D\) is nonempty. Then the graph obtained from \(G\) by contracting \(V \setminus D\) to a single vertex is 2-vertex-connected.

public theorem IsVertexConnected.contractOutside {V : Type*} [Fintype V]
    {G : SimpleGraph V} {D : Set V} [Fintype D] (hG : G.IsVertexConnected 2)
    (hDcard : 1 < Fintype.card D) (hDconn : (G.induce D).Connected)
    (hDout : Dᶜ.Nonempty) : (G.contractOutside D).IsVertexConnected 2

Uses 11 · Used by 1

Statement uses\(k\)-vertex-connected graph · Contracting the complement of a vertex set

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\) · Collapsing the complement of a set · Preimages of retained vertices under the collapse map · The collapse map fixes the retained set · The collapse map sends the complement to the contraction vertex · The collapse map is surjective · Contraction preserves adjacency among retained vertices · Characterization of 2-vertex-connected graphs

Used byStrengthened Fleischner theorem

TheoremCardinality bound for contracting the complement#✓fully proved

Let \(V\) be a finite set and \(D \subseteq V\). If the complement \(V \setminus D\) has at least two elements, then \(D\) together with one new vertex has fewer elements than \(V\), that is, \(|D| + 1 < |V|\).

This counts the vertices of the graph obtained by contracting \(V \setminus D\) to a single vertex.

public theorem card_contractOutside_lt {V : Type*} [Fintype V] (D : Set V)
    [Fintype D] [Fintype ↥(Dᶜ : Set V)] (hD : 2 ≤ Fintype.card ↥(Dᶜ : Set V)) :
    Fintype.card (Option D) < Fintype.card V

Used by 1

Used byStrengthened Fleischner theorem

DefinitionStrong square cycle at a vertex#✓fully proved

Let \(G\) be a graph on a finite vertex set \(V\) and let \(x \in V\). Then \(G\) has a strong square cycle at \(x\) if the square \(G^2\) of \(G\) has a Hamiltonian cycle that starts and ends at \(x\) and whose two edges at \(x\), its first and its last edge, are edges of \(G\).

public def HasStrongSquareCycle {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) (x : V) : Prop :=
  ∃ p : G.square.Walk x x, p.IsHamiltonianCycle ∧
    G.Adj x p.snd ∧ G.Adj p.penultimate x

Uses 1 · Used by 3

Statement usesSquare of a graph

Used byFleischner's theorem · Strengthened Fleischner theorem · Characterization of strong square cycles

TheoremCharacterization of strong square cycles#✓fully proved

Let \(G\) be a graph on a finite vertex set \(V\) and let \(x \in V\). Then \(G\) has a strong square cycle at \(x\) if and only if the square \(G^2\) of \(G\) has a Hamiltonian cycle \(p\) that starts and ends at \(x\) such that \(x\) is adjacent in \(G\) to the second vertex of \(p\) and the second-to-last vertex of \(p\) is adjacent in \(G\) to \(x\).

public theorem hasStrongSquareCycle_iff {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) (x : V) :
    G.HasStrongSquareCycle x ↔
      ∃ p : G.square.Walk x x, p.IsHamiltonianCycle ∧
        G.Adj x p.snd ∧ G.Adj p.penultimate x

Uses 2

Statement usesStrong square cycle at a vertex · Square of a graph

TheoremStrengthened Fleischner theorem#✓fully proved

Let \(G\) be a finite simple graph that is 2-vertex-connected, that is, \(G\) has at least three vertices and stays connected after deleting at most one vertex. Let \(G^2\) be the square of \(G\): the graph on the same vertices in which two distinct vertices are adjacent if and only if they are adjacent in \(G\) or have a common neighbour in \(G\). Then for every vertex \(x\) of \(G\), the graph \(G^2\) has a Hamiltonian cycle whose two edges at \(x\) are edges of \(G\).

public theorem IsVertexConnected.hasStrongSquareCycle
    {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V}
    (hG : G.IsVertexConnected 2) (x : V) : G.HasStrongSquareCycle x

Uses 32 · Used by 1

Statement usesStrong square cycle at a vertex · \(k\)-vertex-connected graph

Proof usesEdge-indexed multigraph · Incidence · Indexed walk · Eulerian indexed walk · Indexed trail · Edge list of an indexed walk · Edge list of an extended indexed walk · Edges of the forgetful walk · Forgetting edge identities preserves length · From an indexed walk to a walk in the underlying graph · Degree in an edge-indexed multigraph · Disjoint sum of edge-indexed multigraphs · Degrees add under disjoint sums · Handshake lemma for edge-indexed multigraphs · Euler circuits in edge-indexed multigraphs · Incidence is membership in the endpoint pair · Underlying simple graph of an edge-indexed multigraph · Adjacency in the underlying graph · Vertex count of a \(k\)-vertex-connected graph · Contracting the complement preserves 2-connectivity · Říha's cycle lemma · Cycles through each vertex of a 2-vertex-connected graph · Degrees in a 2-vertex-connected graph are at least two · Bound vertices of a closed walk · Cardinality bound for contracting the complement · Contracting the complement of a vertex set · Neighbors of the contraction vertex · Contraction preserves adjacency among retained vertices · Square of a graph · Adjacency in the graph square

Used byFleischner's theorem

TheoremFleischner's theorem#✓fully proved

Let \(G\) be a finite simple graph that is 2-vertex-connected, that is, \(G\) has at least three vertices and stays connected after deleting at most one vertex. Let \(H\) be the square of \(G\): the graph on the same vertices in which two distinct vertices are adjacent if and only if they are adjacent in \(G\) or have a common neighbour in \(G\). Then \(H\) is Hamiltonian: it has a cycle that passes through every vertex exactly once.

theorem fleischner : ∀ {V : Type*} [Fintype V] (G H : SimpleGraph V),
    G.IsVertexConnected 2 →
    (∀ u v : V, H.Adj u v ↔ (u ≠ v ∧ (G.Adj u v ∨ ∃ w, G.Adj u w ∧ G.Adj w v))) →
    @SimpleGraph.IsHamiltonian V (fun a b => Classical.propDecidable _) _ H

Sources

• Herbert Fleischner, "The Square of Every Two-Connected Graph Is Hamiltonian," Journal of Combinatorial Theory, Series B 16 (1974), 29–34, DOI 10.1016/0095-8956(74)90091-4, https://doi.org/10.1016/0095-8956(74)90091-4. Proof: the strengthened vertex-rooted induction of A. Georgakopoulos, "A short proof of Fleischner's theorem", Discrete Math. 309 (2009), 6632–6634.

Uses 6

Statement uses\(k\)-vertex-connected graph

Proof usesStrong square cycle at a vertex · Vertex count of a \(k\)-vertex-connected graph · Strengthened Fleischner theorem · Characterization of the graph square · Square of a graph

15 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.