Theorems · Definition · combinatorics

SimpleGraph.Walk.induce

{V : Type u} →
  {G : SimpleGraph V} →
    (s : Set V) →
      {u v : V} → (w : G.Walk u v) → (hw : ∀ x ∈ w.support, x ∈ s) → (SimpleGraph.induce s G).Walk ⟨u, ⋯⟩ ⟨v, ⋯⟩

A walk in G which is fully contained in a set s of vertices lifts to a walk of G[s].

Defined in

Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Cited by

9 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound