Vertex deletion and 2-connectivity

Deleting a vertex from Mathlib's multigraph Graph α β, and the blueprint's notion of a 2-connected graph.

Vertex deletion is Mathlib's

Mathlib already has it: Graph.deleteVerts G X = G.induce (V(G) \ X), in Mathlib/Combinatorics/Graph/Delete.lean, with V(G.deleteVerts X) = V(G) \ X and E(G.deleteVerts X) = {e | ∃ x y, G.IsLink e x y ∧ x ∉ X ∧ y ∉ X} — an edge with an end in X is gone, which is exactly what is wanted. Nothing here redefines it; G.deleteVerts {x} is the deletion of one vertex, and what this file adds is the transfer of walks across it, which Mathlib has no notion of.

Two of those transfers are the whole story, and both are corollaries of Graph.IsWalk.anti:

• Graph.IsWalk.deleteVerts_singleton — a walk that never visits x is a walk of G - x. The edges of such a walk automatically survive, because the ends of an edge of a walk are vertices the walk visits.
• Graph.IsWalk.notMem_of_inc_of_deleteVerts — a walk in G - x cannot have used an edge at x; there are none left to use. This is how an argument that routes around a vertex ends up avoiding a named edge, and it is what makes Graph.IsTwoConnected.no_bridge short.

Deleting a vertex the graph does not have changes nothing — G.deleteVerts {x} = G on the nose (Graph.deleteVerts_singleton_eq_self), since V(G) \ {x} = V(G). That equation is what makes the union lemma's hard case disappear.

At least three vertices

The counting clause of 2-connectivity is carried by Graph.HasThreeVertices, "three pairwise distinct vertices", rather than by 3 ≤ V(G).ncard. The two agree on a finite graph, but the existential form is monotone with no finiteness hypothesis (Graph.HasThreeVertices.mono), and monotonicity is precisely what Graph.IsTwoConnected.union needs: the union of two graphs is not known to be finite at the point where its third vertex is produced. Set.ncard is 0 on an infinite set, so 3 ≤ V(G).ncard would additionally make every infinite graph fail to be 2-connected, which is not the intent of the convention.

What consumers actually use is never the clause itself but Graph.HasThreeVertices.exists_ne_ne — any two vertices leave a third over. Graph.hasThreeVertices_iff_ncard is the bridge back to the count, for a consumer that has one.

The convention, verbatim, and what it costs

Graph.IsTwoConnected is the blueprint's definition word for word (§"Plane graphs and the utility graph"): at least three vertices, connected, and still connected after any one vertex is deleted. Two consequences the blueprint calls out are recorded here as theorems rather than as prose:

• the one-edge graph is not 2-connected, and
• a two-vertex cycle — two parallel edges — is a cycle without being 2-connected.

Both are instances of Graph.not_isTwoConnected_banana: Graph.banana u v F has only the two vertices u and v whatever F is, so it fails the counting clause. Two-vertex cycles do occur in the development, as face boundaries inside a larger 2-connected graph, and this is the theorem that says they are not themselves 2-connected. (No cycle is named here: this file must not depend on the cycle module.)

Union

Mathlib's Mathlib/Combinatorics/Graph/Lattice.lean provides only the infimum of two graphs — there is no union in this version of Mathlib — so Graph.union is defined here. On an edge belonging to both graphs, G's ends win:

(G.union H).IsLink e x y ↔ G.IsLink e x y ∨ (e ∉ E(G) ∧ H.IsLink e x y)

which makes the definition total. It has to be resolved somehow: two graphs may disagree about the ends of a shared edge name, and then no graph has both as subgraphs. When the two graphs are Graph.Compatible — in particular when both are subgraphs of one graph, via Graph.Compatible.of_le_le, which is the only way the plane layer forms unions — the disjunction collapses to the naive one (Graph.Compatible.union_isLink) and both graphs are subgraphs of the union.

Blueprint

• Graph.IsTwoConnected — the definition in §"Plane graphs and the utility graph": "a finite graph is 2-connected if it has at least three vertices, is connected, and remains connected after deletion of any one vertex".
• Graph.IsTwoConnected.no_cut_vertex — "with this convention a 2-connected graph has no cut vertex".
• Graph.not_isTwoConnected_banana — "the one-edge graph is not 2-connected", and the same computation for the two-vertex cycle of the next paragraph.
• Graph.IsTwoConnected.no_bridge — "A 2-connected graph has no bridge", the step of lem:subdivision-ear-preserve (a) that the ear decomposition runs on. Stated as "deleting the edge leaves its ends connected", which is the form lem:cycle-criterion consumes; the cycle itself is built elsewhere.
• Graph.IsTwoConnected.union — lem:union-two-connected, "if two finite 2-connected graphs have at least two vertices in common, their union is 2-connected".

Deleting one vertex

theorem Graph.mem_deleteVerts_singleton {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} : y ∈ (G.deleteVerts {x}).vertexSet ↔ y ∈ G.vertexSet ∧ y ≠ x

theorem Graph.mem_deleteVerts_singleton_of_ne {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (hy : y ∈ G.vertexSet) (hyx : y ≠ x) : y ∈ (G.deleteVerts {x}).vertexSet

theorem Graph.deleteVerts_singleton_eq_self {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (hx : x ∉ G.vertexSet) : G.deleteVerts {x} = G

Deleting a vertex the graph does not have leaves the graph alone — on the nose, not merely up to isomorphism, because V(G) \ {x} is literally V(G).

theorem Graph.deleteVerts_mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G ≤ H) (X : Set α) : G.deleteVerts X ≤ H.deleteVerts X

Deleting the same vertices from both sides of an inclusion keeps it.

Walks across a vertex deletion

theorem Graph.IsWalk.deleteVerts_singleton {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v x : α} {W : List β} (h : G.IsWalk u W v) (hx : x ∉ G.walkVertices u W) : (G.deleteVerts {x}).IsWalk u W v

A walk that never visits x survives the deletion of x. Its edges need no separate argument: the two ends of an edge the walk takes are vertices the walk visits.

theorem Graph.IsWalk.notMem_of_inc_of_deleteVerts {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v x : α} {e : β} {W : List β} (h : (G.deleteVerts {x}).IsWalk u W v) (hx : G.Inc e x) : e ∉ W

A walk in G - x never takes an edge at x — there are none left to take.

theorem Graph.Reaches.deleteEdges_of_deleteVerts {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v x : α} {e : β} (h : (G.deleteVerts {x}).Reaches u v) (hx : G.Inc e x) : (G.deleteEdges {e}).Reaches u v

The bridge between the two deletions: a walk that routes around a vertex x cannot have used an edge incident to x, so it is still there after that edge is deleted.

theorem Graph.Connected.deleteVerts_singleton_of_notMem {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (h : G.Connected) (hx : x ∉ G.vertexSet) : (G.deleteVerts {x}).Connected

Connectedness is unharmed by deleting a vertex the graph does not have.

Cut vertices

def Graph.IsCutVertex {α : Type u_1} {β : Type u_2} (G : Graph α β) (x : α) : Prop

A vertex whose deletion disconnects the graph.

Equations

• G.IsCutVertex x = (x ∈ G.vertexSet ∧ ¬(G.deleteVerts {x}).Connected)

At least three vertices

def Graph.HasThreeVertices {α : Type u_1} {β : Type u_2} (G : Graph α β) : Prop

The graph has three pairwise distinct vertices. Stated existentially rather than as 3 ≤ V(G).ncard so that it is monotone with no finiteness hypothesis.

Equations

• G.HasThreeVertices = ∃ a ∈ G.vertexSet, ∃ b ∈ G.vertexSet, ∃ c ∈ G.vertexSet, a ≠ b ∧ a ≠ c ∧ b ≠ c

theorem Graph.hasThreeVertices_iff_ncard {α : Type u_1} {β : Type u_2} {G : Graph α β} (hV : G.vertexSet.Finite) : G.HasThreeVertices ↔ 3 ≤ G.vertexSet.ncard

On a graph with finitely many vertices the clause is the count it is named for. Kept so that a consumer holding a cardinality is not stranded; nothing in this file uses it.

theorem Graph.HasThreeVertices.mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.HasThreeVertices) (hV : G.vertexSet ⊆ H.vertexSet) : H.HasThreeVertices

theorem Graph.HasThreeVertices.exists_ne_ne {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : G.HasThreeVertices) (u v : α) : ∃ w ∈ G.vertexSet, w ≠ u ∧ w ≠ v

Any two vertices leave a third over. This, and not the counting clause itself, is what every consumer of 2-connectivity uses; the two named vertices need not even be vertices of the graph.

Two-connectivity

structure Graph.IsTwoConnected {α : Type u_1} {β : Type u_2} (G : Graph α β) : Prop

The blueprint's convention, verbatim: at least three vertices, connected, and still connected after any one vertex is deleted.

• hasThreeVertices : G.HasThreeVertices

  The graph has at least three vertices.

• connected : G.Connected

  The graph is connected.

• deleteVerts_connected ⦃x : α⦄ : x ∈ G.vertexSet → (G.deleteVerts {x}).Connected

  Deleting any one vertex leaves it connected.

theorem Graph.IsTwoConnected.deleteVerts_connected' {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : G.IsTwoConnected) (x : α) : (G.deleteVerts {x}).Connected

The deletion clause with its hypothesis dropped: deleting a vertex the graph does not have changes nothing, so no consumer has to check membership first.

theorem Graph.IsTwoConnected.no_cut_vertex {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : G.IsTwoConnected) (x : α) : ¬G.IsCutVertex x

With this convention a 2-connected graph has no cut vertex.

theorem Graph.not_isTwoConnected_banana {α : Type u_1} {β : Type u_2} (u v : α) (F : Set β) : ¬(banana u v F).IsTwoConnected

A graph on two vertices is never 2-connected, whatever edges it carries. Two consequences of the convention at once: the one-edge graph is not 2-connected, and a two-vertex cycle — two parallel edges, F a pair — is a cycle without being 2-connected. Such cycles do occur in the development, as face boundaries inside a larger 2-connected graph.

theorem Graph.IsTwoConnected.no_bridge {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} (h : G.IsTwoConnected) (hl : G.IsLink e u v) : (G.deleteEdges {e}).Reaches u v

A 2-connected graph has no bridge, in the form "deleting an edge leaves its two ends connected" — the hypothesis of the cycle criterion.

The blueprint's proof names the two components of G - e and finds a vertex of one of them other than its endpoint. This proof routes around instead, and never mentions a component: a third vertex w exists; the graph without v still joins u to w, and the graph without u still joins w to v; and a walk that survives a vertex deletion cannot have used an edge there, so neither walk used e. A loop needs no argument at all.

The union of two graphs

def Graph.union {α : Type u_1} {β : Type u_2} (G H : Graph α β) : Graph α β

The union of two graphs. On an edge belonging to both, G's ends win — a resolution is needed, since two graphs may disagree about the ends of a shared edge name; for Graph.Compatible graphs, which is the only case the development forms, the disjunction collapses to the naive one.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Graph.vertexSet_union {α : Type u_1} {β : Type u_2} (G H : Graph α β) : (G.union H).vertexSet = G.vertexSet ∪ H.vertexSet

@[simp]

theorem Graph.edgeSet_union {α : Type u_1} {β : Type u_2} (G H : Graph α β) : (G.union H).edgeSet = G.edgeSet ∪ H.edgeSet

theorem Graph.union_isLink {α : Type u_1} {β : Type u_2} {G H : Graph α β} {x y : α} {e : β} : (G.union H).IsLink e x y ↔ G.IsLink e x y ∨ e ∉ G.edgeSet ∧ H.IsLink e x y

theorem Graph.left_le_union {α : Type u_1} {β : Type u_2} (G H : Graph α β) : G ≤ G.union H

theorem Graph.union_le {α : Type u_1} {β : Type u_2} {G H K : Graph α β} (hGK : G ≤ K) (hHK : H ≤ K) : G.union H ≤ K

Two subgraphs of one graph have their union inside it.

theorem Graph.Compatible.right_le_union {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.Compatible H) : H ≤ G.union H

The right-hand graph is a subgraph of the union only when the two agree about their shared edges — without that, no graph has both as subgraphs.

theorem Graph.Compatible.union_isLink {α : Type u_1} {β : Type u_2} {G H : Graph α β} {x y : α} {e : β} (h : G.Compatible H) : (G.union H).IsLink e x y ↔ G.IsLink e x y ∨ H.IsLink e x y

For compatible graphs the union is the naive one.

theorem Graph.Connected.of_two_subgraphs {α : Type u_1} {β : Type u_2} {K G₁ G₂ : Graph α β} {s : α} (h₁ : G₁ ≤ K) (h₂ : G₂ ≤ K) (hV : K.vertexSet ⊆ G₁.vertexSet ∪ G₂.vertexSet) (hc₁ : G₁.Connected) (hc₂ : G₂.Connected) (hs₁ : s ∈ G₁.vertexSet) (hs₂ : s ∈ G₂.vertexSet) : K.Connected

Two connected parts covering a graph and sharing a vertex make it connected. Used twice below — once for the union itself, once for the union with a vertex deleted — and both times the two parts are G and H while the whole is not their union on the nose.

theorem Graph.Compatible.union_connected {α : Type u_1} {β : Type u_2} {G H : Graph α β} {s : α} (h : G.Compatible H) (hG : G.Connected) (hH : H.Connected) (hs : s ∈ G.vertexSet) (hs' : s ∈ H.vertexSet) : (G.union H).Connected

theorem Graph.IsTwoConnected.union {α : Type u_1} {β : Type u_2} {G H : Graph α β} {a b : α} (hcompat : G.Compatible H) (hG : G.IsTwoConnected) (hH : H.IsTwoConnected) (hab : a ≠ b) (haG : a ∈ G.vertexSet) (haH : a ∈ H.vertexSet) (hbG : b ∈ G.vertexSet) (hbH : b ∈ H.vertexSet) : (G.union H).IsTwoConnected

lem:union-two-connected: two 2-connected graphs with at least two vertices in common have 2-connected union.

The blueprint's proof is one sentence — after deleting one vertex, each graph remains connected and at least one common vertex remains. The work is the case where the deleted vertex belongs to only one of the two graphs: the other graph never had it, so nothing was deleted from it, and Graph.deleteVerts_singleton_eq_self makes that a rewriting step rather than an argument.