Theorems · Theorem · combinatorics

SimpleGraph.Walk.map_induce_induceHomOfLE

∀ {V : Type u} {G : SimpleGraph V} {s s' : Set V} (hs : s ⊆ s') {u v : V} (w : G.Walk u v)
  (hw : ∀ x ∈ w.support, x ∈ s),
  SimpleGraph.Walk.map (G.induceHomOfLE hs).toHom (SimpleGraph.Walk.induce s w hw) = SimpleGraph.Walk.induce s' w ⋯

Defined in

Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Cited by

0 results in Mathlib

Foundations

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