Walks and paths in a multigraph

Mathlib's Graph α β carries incidence (G.IsLink e x y) and nothing that moves along it. This file is the bottom of the combinatorial layer: walks, paths, reachability and connectedness, all of which the plane development consumes through one theorem — Graph.IsWalk.contains_path, the blueprint's "shorten an arbitrary walk at repeated vertices".

A walk is a list of edges

G.IsWalk u W v says the edge list W walks from u to v, each edge taken from the vertex the previous one arrived at. It names its edges, not its vertices. That is forced by parallel edges: two edges with the same ends are distinguishable only by name, and a walk along one of them must be able to say which it took — a two-vertex cycle, which the plane layer builds out of a Jordan curve cut at two points, is exactly such a graph. Nothing is lost by naming edges, because an edge determines where taking it arrives (Graph.IsLink.right_unique upstream, Graph.IsWalk.target_unique here).

It is an inductive family, not a recursion over the list. Every consumer argues by induction along the walk, and the inductive gives that directly, naming the waypoint of each step; a recursion fun u (e :: W) v => ∃ w, G.IsLink e u w ∧ IsWalk G w W v would force every proof to generalize the source vertex by hand and to destructure an existential at each step. The relation is built at the source end, since that is the end a list is extended at; concatenation (Graph.IsWalk.append) and reversal (Graph.IsWalk.reverse) are proved here once, and after that no argument has to care.

The empty walk demands x ∈ V(G). This buys the whole file: every vertex a walk visits is a vertex of the graph with no side hypothesis, because Mathlib's Graph already forces the ends of an edge into V(G).

A path carries its own freshness

G.IsPath u W v is a walk with one clause added at each step: the vertex the step departs from is not among those the rest of the path visits. The condition travels with the induction, instead of being imposed afterwards on a separately computed vertex list — which would have to be computed, and would need the graph to be loopless before it was even correct.

Loops

Mathlib's Graph allows an edge with both ends equal; the blueprint's graphs have none. Walks tolerate loops and paths exclude them automatically — no hypothesis on G anywhere in this file. A step of a path from u along e to w requires u ∉ G.walkVertices w W, and w is always in that set, so u ≠ w: the freshness clause already says a path's step is not a loop (Graph.IsPath.not_isLoopAt). Imposing looplessness on the graph instead would put a hypothesis on every statement in the layer to rule out something the definitions already rule out.

Namespace

Declarations live in the root Graph namespace, extending Mathlib's, rather than in Schoenflies: G.IsWalk, hW.append, hP.isWalk are the spellings every consumer wants, and dot notation on a Mathlib type resolves through the type's own namespace.

Blueprint

The blueprint uses finite graphs as an imported foundation (§"Imported facts", Finite graphs: "in a finite connected graph, any two vertices are joined by a simple path, obtained by shortening an arbitrary walk at repeated vertices"). This file supplies that import.

• Graph.IsWalk.contains_path — shortening a walk to a path; used at lem:polygonal-connected ("take a simple path in the resulting finite graph"), lem:finite-polygonal-union ("a simple graph path has the required realization") and lem:skeleton-crosscuts ("the resulting finite graph is connected, so it contains a simple graph path P from a to b").
• Graph.Reaches, Graph.Connected — the connectedness those three lemmas invoke.
• Graph.IsPath.nodup — a simple path repeats no edge; underneath the finiteness arguments that bound a path's length.
• Graph.IsPath.reverse, Graph.IsPath.split — a path backwards, and a path cut in two at a vertex it visits; what lem:subdivision-ear-preserve and lem:relative-ear run on.

The vertices an edge list touches

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

The vertices lying on at least one edge of W.

Equations

• G.coveredVertices W = {x : α | ∃ e ∈ W, G.Inc e x}

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

The vertices a walk from u along W visits: its source, plus the ends of every edge it takes. Defined for any edge list, not just for one that walks — the freshness clause of a path reads it about the rest of the path before that rest is known to be a walk at all.

Equations

• G.walkVertices u W = insert u (G.coveredVertices W)

theorem Graph.mem_coveredVertices_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {W : List β} : x ∈ G.coveredVertices W ↔ ∃ e ∈ W, G.Inc e x

theorem Graph.mem_walkVertices_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {u x : α} {W : List β} : x ∈ G.walkVertices u W ↔ x = u ∨ x ∈ G.coveredVertices W

@[simp]

theorem Graph.coveredVertices_nil {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.coveredVertices [] = ∅

@[simp]

theorem Graph.walkVertices_nil {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} : G.walkVertices u [] = {u}

theorem Graph.mem_coveredVertices {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {e : β} {W : List β} (he : e ∈ W) (hx : G.Inc e x) : x ∈ G.coveredVertices W

theorem Graph.mem_walkVertices_self {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} {W : List β} : u ∈ G.walkVertices u W

theorem Graph.mem_walkVertices_of_mem_covered {α : Type u_1} {β : Type u_2} {G : Graph α β} {u x : α} {W : List β} (hx : x ∈ G.coveredVertices W) : x ∈ G.walkVertices u W

theorem Graph.coveredVertices_mono {α : Type u_1} {β : Type u_2} {G : Graph α β} {W₁ W₂ : List β} (h : W₁ ⊆ W₂) : G.coveredVertices W₁ ⊆ G.coveredVertices W₂

theorem Graph.walkVertices_mono {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} {W₁ W₂ : List β} (h : W₁ ⊆ W₂) : G.walkVertices u W₁ ⊆ G.walkVertices u W₂

@[simp]

theorem Graph.coveredVertices_reverse {α : Type u_1} {β : Type u_2} {G : Graph α β} {W : List β} : G.coveredVertices W.reverse = G.coveredVertices W

@[simp]

theorem Graph.walkVertices_reverse {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} {W : List β} : G.walkVertices u W.reverse = G.walkVertices u W

theorem Graph.coveredVertices_append {α : Type u_1} {β : Type u_2} {G : Graph α β} {W₁ W₂ : List β} : G.coveredVertices (W₁ ++ W₂) = G.coveredVertices W₁ ∪ G.coveredVertices W₂

theorem Graph.coveredVertices_subset_vertexSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {W : List β} : G.coveredVertices W ⊆ G.vertexSet

Every vertex on an edge of the graph is a vertex of the graph.

theorem Graph.walkVertices_subset_vertexSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} {W : List β} (hu : u ∈ G.vertexSet) : G.walkVertices u W ⊆ G.vertexSet

theorem Graph.mem_walkVertices_cons {α : Type u_1} {β : Type u_2} {G : Graph α β} {u w x : α} {e : β} {W : List β} (hl : G.IsLink e u w) (hx : x ∈ G.walkVertices u (e :: W)) : x = u ∨ x ∈ G.walkVertices w W

Moving the visited set across a first step, forwards: a vertex the walk visits is either the vertex it departs from or a vertex the rest of it visits. This is where the step lemma is used — the edge e has only the two ends u and w, so a vertex on e is one of them.

theorem Graph.mem_walkVertices_cons_of_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {u w x : α} {e : β} {W : List β} (hl : G.IsLink e u w) (hx : x ∈ G.walkVertices w W) : x ∈ G.walkVertices u (e :: W)

Moving the visited set across a first step, backwards.

Walks

inductive Graph.IsWalk {α : Type u_1} {β : Type u_2} (G : Graph α β) : α → List β → α → Prop

G.IsWalk u W v : the edges of W, in order, walk from u to v in G. Each edge is taken from the vertex the previous one arrived at; the list is read at its head, so the relation is built at the source end.

• nil {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (hx : x ∈ G.vertexSet) : G.IsWalk x [] x

  Standing still at a vertex of the graph is a walk.

• cons {α : Type u_1} {β : Type u_2} {G : Graph α β} {u w v : α} {e : β} {W : List β} (hl : G.IsLink e u w) (hW : G.IsWalk w W v) : G.IsWalk u (e :: W) v

  Taking an edge from the source of a walk prepends it.

theorem Graph.IsWalk.single {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} (hl : G.IsLink e u v) : G.IsWalk u [e] v

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

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

theorem Graph.IsWalk.edge_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} {W : List β} (h : G.IsWalk u W v) (he : e ∈ W) : e ∈ G.edgeSet

The edges of a walk are edges of the graph.

theorem Graph.IsWalk.edgeSet_subset {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {W : List β} (h : G.IsWalk u W v) (e : β) : e ∈ W → e ∈ G.edgeSet

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

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

Every vertex a walk visits is a vertex of the graph — with no hypothesis, since the empty walk already stands at one.

@[simp]

theorem Graph.isWalk_nil_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} : G.IsWalk u [] v ↔ u = v ∧ u ∈ G.vertexSet

theorem Graph.IsWalk.eq_of_nil {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} (h : G.IsWalk u [] v) : u = v

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

The step lemma, run along a whole walk: naming the edges determines the vertices, so a walk from a given source along a given edge list arrives nowhere else. Its engine is that an edge has only two ends, Graph.IsLink.right_unique, which holds in Mathlib's Graph with no distinctness hypothesis (a loop arrives back where it started, deterministically).

theorem Graph.IsWalk.append {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v w : α} {W₁ W₂ : List β} (h₁ : G.IsWalk u W₁ w) (h₂ : G.IsWalk w W₂ v) : G.IsWalk u (W₁ ++ W₂) v

Walks concatenate, with no side condition.

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

A walk runs backwards along the reverse of its edge list, with no side condition.

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

A walk in a subgraph is a walk in the graph.

theorem Graph.IsWalk.anti {α : Type u_1} {β : Type u_2} {G H : Graph α β} {u v : α} {W : List β} (hHG : H ≤ G) (h : G.IsWalk u W v) (hu : u ∈ H.vertexSet) (hE : ∀ e ∈ W, e ∈ H.edgeSet) : H.IsWalk u W v

A walk of a graph whose edges all survive into a subgraph is a walk of that subgraph. This is the direction a deletion argument needs: an edge is removed, and a walk that never used it is still there.

theorem Graph.IsWalk.crossing {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {W : List β} {S : Set α} (h : G.IsWalk u W v) (hu : u ∈ S) (hv : v ∉ S) : ∃ e ∈ W, ∃ (x : α) (y : α), G.IsLink e x y ∧ x ∈ S ∧ y ∉ S

A walk that starts inside a set of vertices and ends outside it crosses the boundary along one of its own edges.

Paths

inductive Graph.IsPath {α : Type u_1} {β : Type u_2} (G : Graph α β) : α → List β → α → Prop

G.IsPath u W v : a walk from u to v that never returns to a vertex it has left. The condition is carried step by step — the vertex a step departs from is not among those the rest of the path visits — rather than imposed afterwards on a computed vertex list.

• nil {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (hx : x ∈ G.vertexSet) : G.IsPath x [] x

  Standing still at a vertex of the graph is a path.

• cons {α : Type u_1} {β : Type u_2} {G : Graph α β} {u w v : α} {e : β} {W : List β} (hl : G.IsLink e u w) (hW : G.IsPath w W v) (hfresh : u ∉ G.walkVertices w W) : G.IsPath u (e :: W) v

  A step onto a path is allowed when the vertex it departs from is fresh.

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

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

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

theorem Graph.IsPath.edge_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} {W : List β} (h : G.IsPath u W v) (he : e ∈ W) : e ∈ G.edgeSet

theorem Graph.IsPath.single {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} (hl : G.IsLink e u v) (huv : u ≠ v) : G.IsPath u [e] v

One edge between two distinct vertices is a path.

theorem Graph.IsPath.cons_ne {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v w : α} {W : List β} (hW : G.IsPath w W v) (hfresh : u ∉ G.walkVertices w W) : u ≠ w

A path's step never departs from where it arrives: the freshness clause already says so, because a walk always visits its own source.

theorem Graph.IsPath.not_isLoopAt {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} {W : List β} (h : G.IsPath u W v) (he : e ∈ W) (x : α) : ¬G.IsLoopAt e x

A path never takes a loop. This is why nothing in this file has to assume the graph is loopless: a step along a loop would depart from the vertex it arrives at, which the freshness clause forbids.

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

A path takes no edge twice: an edge it took again would put the vertex it departed from back among the ones the rest of the path visits.

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

A path in a subgraph is a path in the graph: the freshness clause reads only which vertices the remaining edges touch, and a subgraph's edges have the same ends there.

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

theorem Graph.IsPath.extend_at_target {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v w : α} {e : β} {P : List β} (h : G.IsPath u P w) (hl : G.IsLink e w v) (hv : v ∉ G.walkVertices u P) : G.IsPath u (P ++ [e]) v

A path grows at its target end. The relation is built at the source end, so this is the direction that has to be worked for; it is what reversal runs on.

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

A path runs backwards over the same edges.

theorem Graph.IsPath.from_visited {α : 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) : ∃ (T : List β), G.IsPath x T v ∧ T ⊆ W

Cutting a path at a vertex it passes through. A path through x has a piece of itself running from x to its target, and that piece uses only the path's own edges. This is the engine of Graph.IsWalk.contains_path: when the next vertex is already on the path built so far, the path is cut there instead of extended, so nothing ever gets longer.

theorem Graph.IsPath.split {α : 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) : ∃ (W₁ : List β) (W₂ : List β), W = W₁ ++ W₂ ∧ G.IsPath u W₁ x ∧ G.IsPath x W₂ v ∧ (x = u ∨ u ∉ G.walkVertices x W₂)

A path splits at any vertex it visits, and the far half never returns to the source. Graph.IsPath.from_visited is the suffix alone; the prefix is the awkward half, since the relation is built at the source end and the prefix is what the induction has to carry forward.

theorem Graph.IsWalk.contains_path {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {W : List β} (h : G.IsWalk u W v) : ∃ (P : List β), G.IsPath u P v ∧ P ⊆ W

Every walk contains a path between the same two vertices, using only the walk's own edges. This is the blueprint's "shorten an arbitrary walk at repeated vertices"; the induction never lengthens anything, because the only alternative to prepending an edge is to cut the path already built (Graph.IsPath.from_visited).

Reachability

def Graph.Reaches {α : Type u_1} {β : Type u_2} (G : Graph α β) (u v : α) : Prop

G.Reaches u v : some walk of G runs from u to v. Stated with a walk rather than a path because walks are what arguments build — they concatenate and reverse with no side condition — and a path is recovered on demand (Graph.Reaches.exists_isPath).

Equations

• G.Reaches u v = ∃ (W : List β), G.IsWalk u W v

theorem Graph.Reaches.left_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} (h : G.Reaches u v) : u ∈ G.vertexSet

theorem Graph.Reaches.right_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} (h : G.Reaches u v) : v ∈ G.vertexSet

theorem Graph.Reaches.refl {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} (hu : u ∈ G.vertexSet) : G.Reaches u u

theorem Graph.Reaches.symm {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} (h : G.Reaches u v) : G.Reaches v u

theorem Graph.Reaches.trans {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v w : α} (h₁ : G.Reaches u v) (h₂ : G.Reaches v w) : G.Reaches u w

theorem Graph.reaches_comm {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} : G.Reaches u v ↔ G.Reaches v u

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

theorem Graph.Reaches.of_adj {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} (h : G.Adj u v) : G.Reaches u v

theorem Graph.Reaches.exists_isPath {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} (h : G.Reaches u v) : ∃ (P : List β), G.IsPath u P v

Whatever a walk reaches, a path reaches.

theorem Graph.Reaches.mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} {u v : α} (hHG : H ≤ G) (h : H.Reaches u v) : G.Reaches u v

Connectedness

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

A graph is connected when it has a vertex and every vertex reaches every other. The nonemptiness clause is not bureaucracy: it is what makes the counting statements about trees true as stated.

Equations

• G.Connected = (G.vertexSet.Nonempty ∧ ∀ ⦃u : α⦄, u ∈ G.vertexSet → ∀ ⦃v : α⦄, v ∈ G.vertexSet → G.Reaches u v)

theorem Graph.Connected.nonempty {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : G.Connected) : G.vertexSet.Nonempty

theorem Graph.Connected.reaches {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} (h : G.Connected) (hu : u ∈ G.vertexSet) (hv : v ∈ G.vertexSet) : G.Reaches u v

theorem Graph.Connected.of_hub {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} (hu : u ∈ G.vertexSet) (h : ∀ v ∈ G.vertexSet, G.Reaches u v) : G.Connected

A graph is connected as soon as one vertex reaches all the others: reachability is symmetric and transitive, so a common hub joins every pair.

theorem Graph.Connected.exists_isPath {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} (h : G.Connected) (hu : u ∈ G.vertexSet) (hv : v ∈ G.vertexSet) : ∃ (P : List β), G.IsPath u P v

In a connected graph any two vertices are joined by a path — the blueprint's imported fact about finite graphs, with the finiteness it does not actually need dropped.

Transferring walks and paths along an inclusion or a deletion

IsWalk.anti above pulls a walk down an inclusion. These are its companions, factored here because both the cycle module and the two-connectivity module reached for them independently.

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

theorem Graph.walkVertices_mono_of_le {α : 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.IsPath.anti {α : Type u_1} {β : Type u_2} {G H : Graph α β} {u v : α} {W : List β} (hHG : H ≤ G) (h : G.IsPath u W v) (hu : u ∈ H.vertexSet) (hE : ∀ e ∈ W, e ∈ H.edgeSet) : H.IsPath u W v

A path of a graph whose edges all survive into a subgraph is a path of that subgraph — the companion of Graph.IsWalk.anti, which it is otherwise identical to. Freshness comes down the inclusion because the subgraph's edges touch no vertices the graph's do not.

theorem Graph.mem_edgeSet_deleteEdges_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} {f : β} : f ∈ (G.deleteEdges F).edgeSet ↔ f ∈ G.edgeSet ∧ f ∉ F

theorem Graph.IsWalk.deleteEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {W : List β} {F : Set β} (h : G.IsWalk u W v) (hW : ∀ f ∈ W, f ∉ F) : (G.deleteEdges F).IsWalk u W v

A walk that avoids the deleted names survives the deletion.