Theorems · Theorem · combinatorics

SimpleGraph.Walk.transfer_append

∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} {w : V} (q : G.Walk v w)
  (hpq : ∀ e ∈ (p.append q).edges, e ∈ H.edgeSet),
  (p.append q).transfer H hpq = (p.transfer H ⋯).append (q.transfer H ⋯)

Defined in

Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Cited by

1 results in Mathlib

Foundations

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