Theorems · Theorem · combinatorics

SimpleGraph.Walk.transfer_transfer

∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet)
  {K : SimpleGraph V} (hp' : ∀ e ∈ (p.transfer H hp).edges, e ∈ K.edgeSet),
  (p.transfer H hp).transfer K hp' = p.transfer K ⋯

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