A path presented as a graph

Schoenflies/Graph/Walk.lean says what it means for an edge list to run through a graph. This file says what it means for a graph to be a path, and — the point of the file — constructs one.

Why the object exists

An ear is a path that gets glued onto a graph, so it has to be a graph itself, not a walk inside one. Graph.IsPathGraph P u W v says that P's own edges, listed in the order W, form a path from u to v and that P's vertices are exactly the ones that path visits. The list W is an index of the predicate rather than an existential: its order is part of the claim, and it is what lets every later argument cut the path at a vertex without first having to sort anything.

Mathlib's Graph α β carries a Set β of edges, not a list, so the correspondence between the two is a clause of the definition (Graph.IsPathGraph.edgeSet_eq) rather than something a list-based graph would give for free.

Constructing one

Graph.pathGraphOf G u W is the subgraph of G spanned by the walk W from u: the vertices the walk visits, and its own edges. Everything else in the file is a hypothesis of the form IsPathGraph; this is where one is produced, and it is what an ear decomposition runs on — a path found inside a big graph has to be turned into a graph before it can be unioned back in.

What the ear argument actually asks

Always the same thing: whatever vertex is deleted, every remaining vertex of the path still reaches one of the two ends (Graph.IsPathGraph.reaches_an_end). The proof is uniform in the deleted vertex c, with no case split on whether c is an end, an interior vertex or off the path at all:

• if c is on the path, cut there (Graph.IsPath.split); each remaining vertex lies on one of the two halves, and a half runs to its far end without meeting the cut, because the split's last clause says the far half never returns to the source;
• if c is not on the path, cut at the vertex itself and reverse the near half.

Both branches go through the same two lemmas, Graph.IsPath.reaches_target_of_ne_source and its mirror, so the interior case has no separate content.

Blueprint

• Graph.IsPathGraph — the object called "a path P" in Lemma lem:subdivision-ear-preserve (b) ("if P is a path whose distinct endpoints lie in G … then G ∪ P is 2-connected") and "an ear" in Lemma lem:relative-ear.
• Graph.IsPathGraph.reaches_an_end — the blueprint's "every component of P - x is attached to G - x at one of the two endpoints of P; when x is an endpoint, the remainder of P is attached at the other endpoint", both sentences at once.
• Graph.pathGraphOf — the "shortest path through L between two such neighbors is an ear" of lem:relative-ear: a path of the ambient graph, presented as a graph.

Nothing here mentions 2-connectivity; the union of a 2-connected graph with an ear is a later module.

Namespace

Root Graph, as fixed by Schoenflies/Graph/Walk.lean, so that h.reaches_an_end and G.pathGraphOf u W resolve by dot notation.

Walks and vertex deletion

Mathlib's Graph.deleteVerts takes a set; a single deleted vertex is {c}.

theorem Graph.coveredVertices_anti {α : Type u_1} {β : Type u_2} {G H : Graph α β} {W : List β} (hHG : H ≤ G) : H.coveredVertices W ⊆ G.coveredVertices W

Pushing the visited set down an inclusion: a subgraph's edges have ends the big graph's edges have too. This is the direction the freshness clause of a path travels in, and the whole content of Graph.IsPath.anti.

theorem Graph.walkVertices_anti {α : Type u_1} {β : Type u_2} {G H : Graph α β} {u : α} {W : List β} (hHG : H ≤ G) : H.walkVertices u W ⊆ G.walkVertices u W

theorem Graph.IsWalk.avoiding {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v c : α} {W : List β} (h : G.IsWalk u W v) (hc : c ∉ G.walkVertices u W) : (G.deleteVerts {c}).IsWalk u W v

A walk that never visits c survives the deletion of c. Every deletion argument in the ear layer reduces to this.

theorem Graph.IsWalk.reverse_walkVertices {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {W : List β} (h : G.IsWalk u W v) : G.walkVertices v W.reverse = G.walkVertices u W

Reversal does not change which vertices a walk visits — but it does change the source, so this is not Graph.walkVertices_reverse, which keeps it.

theorem Graph.walkVertices_append_subset {α : Type u_1} {β : Type u_2} {G : Graph α β} {u w : α} {W₁ W₂ : List β} : G.walkVertices u (W₁ ++ W₂) ⊆ G.walkVertices u W₁ ∪ G.walkVertices w W₂

Splitting the visited set along a concatenation. Purely about lists: no walk is needed, and the middle vertex w is arbitrary.

Reaching an end of a path after a deletion

theorem Graph.IsPath.reaches_target_of_ne_source {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v x : α} {W : List β} (h : G.IsPath u W v) (hx : x ∈ G.walkVertices u W) (hxu : x ≠ u) : (G.deleteVerts {u}).Reaches x v

A vertex of a path other than its source still reaches the target once the source is deleted: cut the path at the vertex, and the far half never returns to the source.

theorem Graph.IsPath.reaches_source_of_ne_target {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v x : α} {W : List β} (h : G.IsPath u W v) (hx : x ∈ G.walkVertices u W) (hxv : x ≠ v) : (G.deleteVerts {v}).Reaches x u

The mirror image, run on the reversed path.

theorem Graph.IsPath.reaches_an_end {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v x c : α} {W : List β} (h : G.IsPath u W v) (hx : x ∈ G.walkVertices u W) (hxc : x ≠ c) : (G.deleteVerts {c}).Reaches x u ∨ (G.deleteVerts {c}).Reaches x v

Deleting any vertex leaves every other vertex of a path able to reach an end. Uniform in the deleted vertex c: if c is on the path the path is cut there and each remaining vertex sits on a half that runs to that half's far end; if c is off the path the path is cut at the vertex itself and its near half, reversed, runs to the source.

A graph that is a path

structure Graph.IsPathGraph {α : Type u_1} {β : Type u_2} (P : Graph α β) (u : α) (W : List β) (v : α) : Prop

P.IsPathGraph u W v : the graph P is the path from u to v along W. Its own edges are exactly the entries of W, and its vertices are exactly the ones that path visits.

The edge list is an index rather than an existential because its order is used: an argument that deletes a vertex cuts W in two, and a graph whose edges were only a set would have to recover the order first.

• isPath : P.IsPath u W v

  The graph's own edges, in the given order, form a path from one end to the other.

• edgeSet_eq : P.edgeSet = {e : β | e ∈ W}

  The graph has no edges beyond that path's.

• vertexSet_eq : P.vertexSet = P.walkVertices u W

  The graph has no vertices beyond the ones that path visits.

theorem Graph.IsPathGraph.isWalk {α : Type u_1} {β : Type u_2} {P : Graph α β} {u v : α} {W : List β} (h : P.IsPathGraph u W v) : P.IsWalk u W v

theorem Graph.IsPathGraph.mem_walkVertices {α : Type u_1} {β : Type u_2} {P : Graph α β} {u v x : α} {W : List β} (h : P.IsPathGraph u W v) (hx : x ∈ P.vertexSet) : x ∈ P.walkVertices u W

A vertex of a path graph is visited by its path.

theorem Graph.IsPathGraph.mem_vertexSet {α : Type u_1} {β : Type u_2} {P : Graph α β} {u v x : α} {W : List β} (h : P.IsPathGraph u W v) (hx : x ∈ P.walkVertices u W) : x ∈ P.vertexSet

Conversely, whatever the path visits is a vertex.

theorem Graph.IsPathGraph.mem_edgeSet {α : Type u_1} {β : Type u_2} {P : Graph α β} {u v : α} {e : β} {W : List β} (h : P.IsPathGraph u W v) (he : e ∈ W) : e ∈ P.edgeSet

theorem Graph.IsPathGraph.mem_list {α : Type u_1} {β : Type u_2} {P : Graph α β} {u v : α} {e : β} {W : List β} (h : P.IsPathGraph u W v) (he : e ∈ P.edgeSet) : e ∈ W

theorem Graph.IsPathGraph.source_mem {α : Type u_1} {β : Type u_2} {P : Graph α β} {u v : α} {W : List β} (h : P.IsPathGraph u W v) : u ∈ P.vertexSet

theorem Graph.IsPathGraph.target_mem {α : Type u_1} {β : Type u_2} {P : Graph α β} {u v : α} {W : List β} (h : P.IsPathGraph u W v) : v ∈ P.vertexSet

theorem Graph.IsPathGraph.reverse {α : Type u_1} {β : Type u_2} {P : Graph α β} {u v : α} {W : List β} (h : P.IsPathGraph u W v) : P.IsPathGraph v W.reverse u

A path graph read from the other end.

theorem Graph.IsPathGraph.connected {α : Type u_1} {β : Type u_2} {P : Graph α β} {u v : α} {W : List β} (h : P.IsPathGraph u W v) : P.Connected

A path graph is connected: every vertex is visited, so the path's own prefix runs to it from the source.

theorem Graph.IsPathGraph.reaches_an_end {α : Type u_1} {β : Type u_2} {P : Graph α β} {u v x c : α} {W : List β} (h : P.IsPathGraph u W v) (hx : x ∈ P.vertexSet) (hxc : x ≠ c) : (P.deleteVerts {c}).Reaches x u ∨ (P.deleteVerts {c}).Reaches x v

Whatever vertex is deleted, every remaining vertex of a path graph still reaches one of its two ends. This is what the ear argument turns on: the ear's two ends are the only vertices it shares with the graph it is glued to, so a surviving vertex of the ear has to reach one of them inside the ear itself.

Constructing a path graph

def Graph.pathGraphOf {α : Type u_1} {β : Type u_2} (G : Graph α β) (u : α) (W : List β) : Graph α β

The subgraph of G spanned by the walk W from u: the vertices that walk visits, carrying exactly the walk's own edges.

This is the construction an ear decomposition needs — a path found inside a big graph, turned into a graph of its own so that it can be unioned back in. It is built from Mathlib's Graph.domRestrict and Graph.induce, so that Graph.pathGraphOf_le is almost free.

Equations

• G.pathGraphOf u W = (G.restrict {e : β | e ∈ W}).induce (G.walkVertices u W)

@[simp]

theorem Graph.pathGraphOf_vertexSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} {W : List β} : (G.pathGraphOf u W).vertexSet = G.walkVertices u W

@[simp]

theorem Graph.pathGraphOf_isLink {α : Type u_1} {β : Type u_2} {G : Graph α β} {u x y : α} {e : β} {W : List β} : (G.pathGraphOf u W).IsLink e x y ↔ e ∈ W ∧ G.IsLink e x y ∧ x ∈ G.walkVertices u W ∧ y ∈ G.walkVertices u W

theorem Graph.mem_vertexSet_pathGraphOf_self {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} {W : List β} : u ∈ (G.pathGraphOf u W).vertexSet

theorem Graph.pathGraphOf_le {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {W : List β} (h : G.IsWalk u W v) : G.pathGraphOf u W ≤ G

The spanned subgraph really is a subgraph.

theorem Graph.pathGraphOf_edgeSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {W : List β} (h : G.IsWalk u W v) : (G.pathGraphOf u W).edgeSet = {e : β | e ∈ W}

Its edges are exactly the walk's. One inclusion is the definition; the other needs the walk, to know that an entry of W is an edge of G at all and that its ends are visited.

theorem Graph.coveredVertices_pathGraphOf {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} {W : List β} : (G.pathGraphOf u W).coveredVertices W = G.coveredVertices W

The spanned subgraph visits the same vertices as the ambient graph does along W: its edges are the same edges, joining the same pairs. No walk is needed — an end of an edge of W is visited by definition, so it survives the induced subgraph.

theorem Graph.walkVertices_pathGraphOf {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} {W : List β} : (G.pathGraphOf u W).walkVertices u W = G.walkVertices u W

theorem Graph.IsWalk.pathGraphOf {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {W : List β} (h : G.IsWalk u W v) : (G.pathGraphOf u W).IsWalk u W v

The walk runs inside the subgraph it spans.

theorem Graph.IsPath.pathGraphOf {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {W : List β} (h : G.IsPath u W v) : (G.pathGraphOf u W).IsPath u W v

The path runs inside the subgraph it spans.

theorem Graph.IsPath.isPathGraph_pathGraphOf {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {W : List β} (h : G.IsPath u W v) : (G.pathGraphOf u W).IsPathGraph u W v

A path of G spans a path graph. This is the construction the whole file exists for: the object every Graph.IsPathGraph hypothesis elsewhere is discharged by.

Finiteness

A walk visits finitely many vertices and takes finitely many edges, so the graph it spans is finite with no hypothesis on the ambient graph.

theorem Graph.walkVertices_cons {α : Type u_1} {β : Type u_2} {G : Graph α β} {u w : α} {e : β} {W : List β} (hl : G.IsLink e u w) : G.walkVertices u (e :: W) = insert u (G.walkVertices w W)

A step of a walk adds exactly one vertex to the visited set.

theorem Graph.IsWalk.finite_walkVertices {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {W : List β} (h : G.IsWalk u W v) : (G.walkVertices u W).Finite

theorem Graph.IsWalk.finite_vertexSet_pathGraphOf {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {W : List β} (h : G.IsWalk u W v) : (G.pathGraphOf u W).vertexSet.Finite

The graph spanned by a walk has finitely many vertices, whatever the ambient graph. Stated as a Set.Finite rather than as a Graph.Finite instance so that this file does not have to depend on Schoenflies/Graph/Degree.lean; the two halves build one in a line.

theorem Graph.IsWalk.finite_edgeSet_pathGraphOf {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {W : List β} (h : G.IsWalk u W v) : (G.pathGraphOf u W).edgeSet.Finite