Theorems · Theorem · combinatorics

SimpleGraph.Walk.getVert_takeUntil

∀ {V : Type u} {G : SimpleGraph V} {w : V} [inst : DecidableEq V] {u v : V} {n : ℕ} {p : G.Walk u v}
  (hw : w ∈ p.support), n ≤ (p.takeUntil w hw).length → (p.takeUntil w hw).getVert n = p.getVert n

Defined in

Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Cited by

4 results in Mathlib

Foundations

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

Assumes

DecidableEq