Theorems · Theorem · combinatorics

SimpleGraph.Walk.transfer.congr_simp

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

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