Cut vertices of simple graphs

A vertex of a simple graph is a cut vertex when deleting it separates two vertices that were previously connected. The predicate is defined through the native multigraph cut-vertex API for Graph.ofSimpleGraph, and SimpleGraph.isCutVertex_iff_exists_forall_walk_mem_support restates it with walks of the simple graph itself: a cut vertex lies on every walk between two other mutually reachable vertices. Conversely, Graph.isCutVertex_iff_toSimpleGraph_isCutVertex identifies the cut vertices of a multigraph with those of its underlying simple graph on the actual vertices, so loops and parallel edges do not affect cut vertices.

For a vertex set inducing a connected graph without cut vertices, any two of its vertices other than a given vertex are joined by a walk inside the set avoiding it (SimpleGraph.exists_walk_forall_mem_support_mem_and_ne); conversely, such walks rule out cut vertices (SimpleGraph.not_isCutVertex_induce_of_exists_walk). Together these give the ear lemma SimpleGraph.Walk.IsPath.not_isCutVertex_induce_union_support: adding the vertices of a path between two vertices of such a set preserves the absence of cut vertices (R. Diestel, Graph Theory, 5th ed., Graduate Texts in Mathematics 173, Springer, 2017, Section 3.1).

def SimpleGraph.IsCutVertex {V : Type u} (G : SimpleGraph V) (v : V) : Prop

A vertex of a simple graph is a cut vertex when deleting it separates two vertices that were previously connected.

theorem SimpleGraph.isCutVertex_def {V : Type u} (G : SimpleGraph V) (v : V) : G.IsCutVertex v ↔ (Graph.ofSimpleGraph G).IsCutVertex v

The cut-vertex predicate for a simple graph is the native multigraph predicate after applying Graph.ofSimpleGraph.

theorem SimpleGraph.isCutVertex_iff_exists_forall_walk_mem_support {V : Type u} {G : SimpleGraph V} {v : V} : G.IsCutVertex v ↔ ∃ (u : V) (w : V), u ≠ v ∧ w ≠ v ∧ G.Reachable u w ∧ ∀ (p : G.Walk u w), v ∈ p.support

A vertex is a cut vertex exactly when it lies on every walk between some two other vertices that are reachable from each other.

theorem SimpleGraph.IsCutVertex.not_isIsolated {V : Type u} {G : SimpleGraph V} {v : V} (h : G.IsCutVertex v) : ¬G.IsIsolated v

A cut vertex is not isolated.

theorem SimpleGraph.Reachable.exists_walk_notMem_support_of_not_isCutVertex {V : Type u} {G : SimpleGraph V} {a z x : V} (h : G.Reachable a z) (hx : ¬G.IsCutVertex x) (hax : a ≠ x) (hzx : z ≠ x) : ∃ (p : G.Walk a z), x ∉ p.support

If x is not a cut vertex, then two vertices other than x that are reachable from each other are joined by a walk avoiding x.

theorem SimpleGraph.not_isCutVertex_induce_singleton {V : Type u} (G : SimpleGraph V) (v : V) (w : ↑{v}) : ¬(induce {v} G).IsCutVertex w

A graph induced on a singleton has no cut vertex.

@[simp]

theorem SimpleGraph.not_isCutVertex_induce_pair {V : Type u} (G : SimpleGraph V) (u v : V) (w : ↑{u, v}) : ¬(induce {u, v} G).IsCutVertex w

A graph induced on a pair of vertices has no cut vertex.

Induced graphs without cut vertices

theorem SimpleGraph.exists_walk_forall_mem_support_mem_and_ne {V : Type u} {G : SimpleGraph V} {B : Set V} (hconn : (induce B G).Connected) (hcut : ∀ (v : ↑B), ¬(induce B G).IsCutVertex v) {a z x : V} (ha : a ∈ B) (hz : z ∈ B) (hax : a ≠ x) (hzx : z ≠ x) : ∃ (p : G.Walk a z), ∀ y ∈ p.support, y ∈ B ∧ y ≠ x

If a vertex set induces a connected graph without cut vertices, then any two of its vertices other than x are joined by a walk of G inside the set avoiding x.

theorem SimpleGraph.not_isCutVertex_induce_of_exists_walk {V : Type u} {G : SimpleGraph V} {B : Set V} (h : ∀ x ∈ B, ∀ a ∈ B, ∀ b ∈ B, a ≠ x → b ≠ x → ∃ (p : G.Walk a b), ∀ y ∈ p.support, y ∈ B ∧ y ≠ x) (x : ↑B) : ¬(induce B G).IsCutVertex x

A vertex set induces a graph without cut vertices when, for each vertex x, any two other vertices of the set are joined by a walk of G inside the set avoiding x.

theorem SimpleGraph.Walk.IsPath.not_isCutVertex_induce_union_support {V : Type u} {G : SimpleGraph V} {B : Set V} (hconn : (induce B G).Connected) (hcut : ∀ (v : ↑B), ¬(induce B G).IsCutVertex v) {a b : V} {p : G.Walk a b} (hp : p.IsPath) (ha : a ∈ B) (hb : b ∈ B) (x : ↑(B ∪ {y : V | y ∈ p.support})) : ¬(induce (B ∪ {y : V | y ∈ p.support}) G).IsCutVertex x

Adding an ear. If a vertex set induces a connected graph without cut vertices, then adding the vertices of a path between two of its vertices gives a vertex set whose induced graph still has no cut vertex.

theorem Graph.isCutVertex_iff_toSimpleGraph_isCutVertex {α : Type u_1} {β : Type u_2} {G : Graph α β} {v : α} (hv : v ∈ G.vertexSet) : G.IsCutVertex v ↔ G.toSimpleGraph.IsCutVertex ⟨v, hv⟩

A native multigraph cut vertex is a cut vertex of the underlying simple graph on the actual vertices.