theorem
reverse_cons_length
{V : Type}
{G : SimpleGraph V}
(a : V)
(v₀ : V)
(w : V)
(p' : G.Walk a w)
(p : G.Walk v₀ w)
(h : G.Adj v₀ a)
{k : ℕ}
(hp : p.length = k.succ)
(hp' : p = SimpleGraph.Walk.cons h p')
:
p'.length = k
theorem
vertex_in_walk_induction
{V : Type}
{G : SimpleGraph V}
{S : Set V}
{w : V}
(hw : w ∉ S)
(n : ℕ)
(t : V)
:
theorem
vertex_in_walk
{V : Type}
{G : SimpleGraph V}
(S : Set V)
(w : V)
(t : V)
(hw : w ∉ S)
(ht : t ∈ S)
(p : G.Walk t w)
:
∃ (a : V), ∃ u ∈ S, G.Adj u a ∧ a ∉ S