English
If a path p in G from v to w avoids a set s of edges, then the path obtained by deleting s from p is still a path.
Русский
Если путь p в G от v к w не использует ребра из множества s, то путь, полученный удалением ребер s из p, остаётся путём.
LaTeX
$$$\\\\forall {V} (G : SimpleGraph V) {v w : V} (s : Set (Sym2 V)) {p : G.Walk v w}, \\\\text{p.IsPath} \\\\Rightarrow \\\\forall (hp : \\\\forall e, e \\\\in p.edges \\\\Rightarrow e \\\\notin s), (p.toDeleteEdges s hp).IsPath$$
Lean4
protected theorem transfer {q : G.Walk u u} (qc : q.IsCycle) (hq) : (q.transfer H hq).IsCycle := by
cases q with
| nil => simp at qc
| cons _ q =>
simp only [edges_cons, List.mem_cons, forall_eq_or_imp] at hq
simp only [Walk.transfer, cons_isCycle_iff, edges_transfer q hq.2] at qc ⊢
exact ⟨qc.1.transfer hq.2, qc.2⟩
