Documentation

Acmoi.Exercise4_2

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 : wS) (n : ) (t : V) :
t S∀ (p : G.Walk t w), p.length = n∃ (a : V), uS, G.Adj u a aS
theorem vertex_in_walk {V : Type} {G : SimpleGraph V} (S : Set V) (w : V) (t : V) (hw : wS) (ht : t S) (p : G.Walk t w) :
∃ (a : V), uS, G.Adj u a aS