English
If x lies in the support of a nonempty walk p, then there exists a vertex y in the walk's support adjacent to x.
Русский
Если вершина x встречается в поддержке непустого маршрута p, то существует вершина y также в поддержке маршрута, такая что x смежна y.
LaTeX
$$$\forall G\,\forall u\forall v\, (p : G.Walk u v) (hp : \neg p.Nil) (x : V) (hx : x \in p.support), \exists y \in p.support, G.Adj x y$$$
Lean4
theorem adj_of_mem_walk_support {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (hp : ¬p.Nil) {x : V}
(hx : x ∈ p.support) : ∃ y ∈ p.support, G.Adj x y := by
induction p with
| nil => exact (hp Walk.Nil.nil).elim
| @cons u v w h p ih =>
cases List.mem_cons.mp hx with
| inl hxu =>
rw [hxu]
exact ⟨v, ⟨((Walk.cons h p).mem_support_iff).mpr (Or.inr p.start_mem_support), h⟩⟩
| inr hxp =>
cases Decidable.em p.Nil with
| inl hnil =>
rw [Walk.nil_iff_support_eq.mp hnil] at hxp
rw [show (x = v) by simp_all]
exact ⟨u, ⟨(Walk.cons h p).start_mem_support, G.adj_symm h⟩⟩
| inr hnotnil =>
obtain ⟨y, hy⟩ := ih hnotnil hxp
refine ⟨y, ⟨?_, hy.right⟩⟩
rw [Walk.mem_support_iff]
simp only [Walk.support_cons, List.tail_cons]
exact Or.inr hy.left
