Theorems · Theorem · combinatorics

SimpleGraph.Walk.transfer.eq_def

∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (H : SimpleGraph V) (h : ∀ e ∈ p.edges, e ∈ H.edgeSet),
  p.transfer H h =
    match u, v, p, h with
    | u, .(u), SimpleGraph.Walk.nil, h => SimpleGraph.Walk.nil
    | u, w, SimpleGraph.Walk.cons h p, h_1 => SimpleGraph.Walk.cons ⋯ (p.transfer H ⋯)

Defined in

Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Cited by

0 results in Mathlib

Foundations

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