Theorems · Theorem · combinatorics

SimpleGraph.Walk.support_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.Walk.induce s w hw).support = w.support.attachWith (Membership.mem s) hw

Defined in

Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Cited by

0 results in Mathlib

Foundations

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