Theorems · Definition · combinatorics

SimpleGraph.Walk.IsPath.pathGraphCopy

{V : Type u_3} →
  [DecidableEq V] →
    {G : SimpleGraph V} → {u v : V} → {w : G.Walk u v} → w.IsPath → (SimpleGraph.pathGraph (w.length + 1)).Copy G

A path induces an injective homomorphism from a path graph to the graph

Defined in

Mathlib.Combinatorics.SimpleGraph.Hasse

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEq