Theorems · Theorem · combinatorics

SimpleGraph.Walk.transfer_eq_map_ofLE

∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet)
  (GH : G ≤ H), p.transfer H hp = SimpleGraph.Walk.map (SimpleGraph.Hom.ofLE GH) p

Defined in

Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Cited by

1 results in Mathlib

Foundations

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