toDeleteEdge — Mathlib

English

Deleting a single edge e from a walk p yields a walk in the graph with edge e removed, provided p does not contain e.

Русский

Удаление одной дуги e из обхода p даёт обход в графе без ребра e, если p не содержит e.

LaTeX

$$toDeleteEdge e p hp : (G.deleteEdges {e}).Walk v w$$

Lean4

/-- Given a walk that avoids an edge, create a walk in the subgraph with that edge deleted.
This is an abbreviation for `SimpleGraph.Walk.toDeleteEdges`. -/
abbrev toDeleteEdge (e : Sym2 V) (p : G.Walk v w) (hp : e ∉ p.edges) : (G.deleteEdges { e }).Walk v w :=
  p.toDeleteEdges { e } (fun e' => by contrapose!; simp +contextual [hp])

Похожие утверждения