Theorems · Theorem · combinatorics

SimpleGraph.Walk.induce_cons

∀ {V : Type u} {G : SimpleGraph V} {u v u' : V} {s : Set V} (huu' : G.Adj u u') (w : G.Walk u' v)
  (hw : ∀ x ∈ (SimpleGraph.Walk.cons huu' w).support, x ∈ s),
  SimpleGraph.Walk.induce s (SimpleGraph.Walk.cons huu' w) hw = SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.induce s w ⋯)

Defined in

Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Cited by

0 results in Mathlib

Foundations

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