Theorems · Theorem · combinatorics

SimpleGraph.Walk.map_append

∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v w : V} (p : G.Walk u v)
  (q : G.Walk v w), SimpleGraph.Walk.map f (p.append q) = (SimpleGraph.Walk.map f p).append (SimpleGraph.Walk.map f q)

Defined in

Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Cited by

2 results in Mathlib

Foundations

Depth 9 from the axioms · uses propext