Theorems · Theorem · combinatorics

SimpleGraph.Walk.IsPath.neighborSet_toSubgraph_internal

∀ {V : Type u} {G : SimpleGraph V} {v u : V} {i : ℕ} {p : G.Walk u v},
  p.IsPath → i ≠ 0 → i < p.length → p.toSubgraph.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)}

Defined in

Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Cited by

1 results in Mathlib

Foundations

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