Theorems · Definition · combinatorics

SimpleGraph.Walk.toDeleteEdges

{V : Type u} →
  {G : SimpleGraph V} →
    (s : Set (Sym2 V)) → {v w : V} → (p : G.Walk v w) → (∀ e ∈ p.edges, e ∉ s) → (G.deleteEdges s).Walk v w

Given a walk that avoids a set of edges, produce a walk in the graph with those edges deleted.

Defined in

Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Cited by

8 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound