Vertex connectivity

Definition\(k\)-vertex-connected graph#✓fully proved

Let \(k\) be a natural number. A simple graph \(G\) on a finite vertex set \(V\) is \(k\)-vertex-connected if \(V\) has more than \(k\) elements and, for every set \(S\) of fewer than \(k\) vertices, the subgraph of \(G\) induced on \(V \setminus S\) is connected.

public def IsVertexConnected {V : Type*} [Fintype V] (k : ℕ) (G : SimpleGraph V) : Prop :=
  k < Fintype.card V ∧
    ∀ S : Finset V, S.card < k → (G.induce (S : Set V)ᶜ).Connected

Used by 14

Used byContracting the complement preserves 2-connectivity · Fleischner's theorem · Strengthened Fleischner theorem · Říha's cycle lemma · Prism-Hamiltonicity conjecture for 3-connected planar graphs · Minimum degree in the square of a 2-connected graph · Vertex count of a \(k\)-vertex-connected graph · A \(k\)-vertex-connected graph with \(k \ge 1\) is connected · Deleting one vertex from a \(k\)-vertex-connected graph with \(k \ge 2\) · Deleting fewer than \(k\) vertices from a \(k\)-vertex-connected graph · Cycles through each vertex of a 2-vertex-connected graph · Characterization of \(k\)-vertex-connectivity by vertex deletion · Characterization of 2-vertex-connected graphs · Degrees in a 2-vertex-connected graph are at least two

TheoremCharacterization of \(k\)-vertex-connectivity by vertex deletion#✓fully proved

Let \(k\) be a natural number and let \(G\) be a simple graph on a finite vertex set \(V\). Then \(G\) is \(k\)-vertex-connected if and only if \(V\) has more than \(k\) elements and, for every set \(S\) of fewer than \(k\) vertices, the subgraph of \(G\) induced on \(V \setminus S\) is connected.

public theorem isVertexConnected_iff {V : Type*} [Fintype V] {k : ℕ} {G : SimpleGraph V} :
    G.IsVertexConnected k ↔
      k < Fintype.card V ∧
        ∀ S : Finset V, S.card < k → (G.induce (S : Set V)ᶜ).Connected

Uses 1

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

TheoremVertex count of a \(k\)-vertex-connected graph#✓fully proved

Let \(k\) be a natural number. If a simple graph \(G\) on a finite vertex set \(V\) is \(k\)-vertex-connected, then \(V\) has more than \(k\) elements.

public theorem IsVertexConnected.card_gt {V : Type*} [Fintype V] {k : ℕ}
    {G : SimpleGraph V} (hG : G.IsVertexConnected k) : k < Fintype.card V

Uses 1 · Used by 4

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

Used byFleischner's theorem · Strengthened Fleischner theorem · Characterization of 2-vertex-connected graphs · Degrees in a 2-vertex-connected graph are at least two

TheoremDeleting fewer than \(k\) vertices from a \(k\)-vertex-connected graph#✓fully proved

Let \(k\) be a natural number and let \(G\) be a \(k\)-vertex-connected simple graph on a finite vertex set \(V\). Then for every set \(S\) of fewer than \(k\) vertices, the subgraph of \(G\) induced on \(V \setminus S\) is connected.

public theorem IsVertexConnected.connected_induce_compl {V : Type*} [Fintype V] {k : ℕ}
    {G : SimpleGraph V} (hG : G.IsVertexConnected k) (S : Finset V) (hS : S.card < k) :
    (G.induce (S : Set V)ᶜ).Connected

Uses 1 · Used by 3

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

Used byMinimum degree in the square of a 2-connected graph · A \(k\)-vertex-connected graph with \(k \ge 1\) is connected · Deleting one vertex from a \(k\)-vertex-connected graph with \(k \ge 2\)

TheoremA \(k\)-vertex-connected graph with \(k \ge 1\) is connected#✓fully proved

Let \(k \ge 1\) be a natural number. Every \(k\)-vertex-connected simple graph on a finite vertex set is connected.

public theorem IsVertexConnected.connected {V : Type*} [Fintype V] {k : ℕ}
    {G : SimpleGraph V} (hG : G.IsVertexConnected k) (hk : 0 < k) : G.Connected

Uses 2 · Used by 4

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

Proof usesDeleting fewer than \(k\) vertices from a \(k\)-vertex-connected graph

Used byContracting the complement preserves 2-connectivity · Říha's cycle lemma · Characterization of 2-vertex-connected graphs · Degrees in a 2-vertex-connected graph are at least two

TheoremDeleting one vertex from a \(k\)-vertex-connected graph with \(k \ge 2\)#✓fully proved

Let \(k \ge 2\) be a natural number and let \(G\) be a \(k\)-vertex-connected simple graph on a finite vertex set \(V\). Then for every vertex \(v\), the subgraph of \(G\) induced on \(V \setminus \{v\}\) is connected.

public theorem IsVertexConnected.connected_compl_singleton {V : Type*} [Fintype V] {k : ℕ}
    {G : SimpleGraph V} (hG : G.IsVertexConnected k) (hk : 1 < k) (v : V) :
    (G.induce (↑({v} : Finset V) : Set V)ᶜ).Connected

Uses 2 · Used by 5

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

Proof usesDeleting fewer than \(k\) vertices from a \(k\)-vertex-connected graph

Used byContracting the complement preserves 2-connectivity · Říha's cycle lemma · Cycles through each vertex of a 2-vertex-connected graph · Characterization of 2-vertex-connected graphs · Degrees in a 2-vertex-connected graph are at least two

TheoremCharacterization of 2-vertex-connected graphs#✓fully proved

A simple graph \(G\) on a finite vertex set \(V\) is 2-vertex-connected if and only if \(V\) has more than two elements, \(G\) is connected, and for every vertex \(v\) the subgraph of \(G\) induced on \(V \setminus \{v\}\) is connected.

public theorem isVertexConnected_two_iff {V : Type*} [Fintype V] {G : SimpleGraph V} :
    G.IsVertexConnected 2 ↔
      2 < Fintype.card V ∧ G.Connected ∧
        ∀ v, (G.induce (↑({v} : Finset V) : Set V)ᶜ).Connected

Uses 4 · Used by 1

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

Proof usesVertex count of a \(k\)-vertex-connected graph · A \(k\)-vertex-connected graph with \(k \ge 1\) is connected · Deleting one vertex from a \(k\)-vertex-connected graph with \(k \ge 2\)

Used byContracting the complement preserves 2-connectivity

TheoremDegrees in a 2-vertex-connected graph are at least two#✓fully proved

Every vertex of a 2-vertex-connected simple graph on a finite vertex set has degree at least two.

public theorem IsVertexConnected.two_le_degree {V : Type*} [Fintype V]
    {G : SimpleGraph V} [DecidableRel G.Adj] (hG : G.IsVertexConnected 2) (v : V) :
    2 ≤ G.degree v

Uses 4 · Used by 3

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

Proof usesVertex count of a \(k\)-vertex-connected graph · A \(k\)-vertex-connected graph with \(k \ge 1\) is connected · Deleting one vertex from a \(k\)-vertex-connected graph with \(k \ge 2\)

Used byStrengthened Fleischner theorem · Minimum degree in the square of a 2-connected graph · Cycles through each vertex of a 2-vertex-connected graph

TheoremCycles through each vertex of a 2-vertex-connected graph#✓fully proved

Let \(G\) be a 2-vertex-connected simple graph on a finite vertex set. Then for every vertex \(x\) of \(G\) there is a cycle in \(G\) that starts and ends at \(x\).

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

Uses 3 · Used by 2

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

Proof usesDeleting one vertex from a \(k\)-vertex-connected graph with \(k \ge 2\) · Degrees in a 2-vertex-connected graph are at least two

Used byStrengthened Fleischner theorem · Říha's cycle lemma

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.