English
Let p be a path in G from v to u, and let h be an edge between u and v that does not occur among the edges of p. Then the walk obtained by prepending h to p is a cycle: (Walk.cons h ↑p).IsCycle.
Русский
Пусть p — путь в G от v к u, и h — ребро u–v, которое не входит в множество ребер пути p. Тогда обход, полученный при добавлении ребра h перед p, образует цикл: (Walk.cons h ↑p).IsCycle.
LaTeX
$$$\forall {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Path v u) (h : G.Adj u v) (he : s(u, v) \notin (p : G.Walk v u).edges), (Walk.cons h \uparrow p).IsCycle$$$
Lean4
theorem cons_isCycle {u v : V} (p : G.Path v u) (h : G.Adj u v) (he : s(u, v) ∉ (p : G.Walk v u).edges) :
(Walk.cons h ↑p).IsCycle := by simp [Walk.isCycle_def, Walk.cons_isTrail_iff, he]
