toDeleteEdges_cons — Mathlib

English

Deleting edges from a cons walk respects the head edge and recursively deletes edges from the tail.

Русский

Удаление рёбер у обхода вида cons сохраняет головное ребро и рекурсивно удаляет рёбра хвоста.

LaTeX

$$toDeleteEdges s (Walk.cons h p) hp = Walk.cons (deleteEdges_adj …) (p.toDeleteEdges s …)$$

Lean4

@[simp]
theorem toDeleteEdges_cons (s : Set (Sym2 V)) {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (hp) :
    (Walk.cons h p).toDeleteEdges s hp =
      Walk.cons (deleteEdges_adj.mpr ⟨h, hp _ (List.Mem.head _)⟩)
        (p.toDeleteEdges s fun _ he => hp _ <| List.Mem.tail _ he) :=
  rfl

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