English
Let G be a simple graph and let h be an edge joining u to v with u adjacent to v. For any walk p from v to w, the walk formed by prepending h, namely cons(h,p), is a trail if and only if p is a trail and the edge s(u,v) is not among the edges of p.
Русский
Пусть G — простой граф, и пусть e=(u,v) смежно соединяет u и v. Пусть p — обход от v к w. Тогда обход, полученный путем добавления ребра e в начало, cons(e,p), является путём без повторов рёбер тогда и только тогда, когда p является путём без повторов рёбер и ребро e не встречается среди рёбер p.
LaTeX
$$$ (\mathrm{cons}(h,p)).\mathrm{IsTrail} \iff p.\mathrm{IsTrail} \land s(u,v)\nmid p.edges $$$
Lean4
@[simp]
theorem cons_isTrail_iff {u v w : V} (h : G.Adj u v) (p : G.Walk v w) :
(cons h p).IsTrail ↔ p.IsTrail ∧ s(u, v) ∉ p.edges := by simp [isTrail_def, and_comm]
