toDeleteEdges — Mathlib

English

The operation toDeleteEdges commutes with copying endpoints: deleting edges after copying endpoints equals copying the result of deletion with updated endpoints.

Русский

Операция toDeleteEdges совместима с копированием концов: удаление ребер после копирования концов равно копированию результата удаления с обновлёнными концами.

LaTeX

$$$\\\\forall {V} {G : SimpleGraph V} {v u u' v'} (s : Set (Sym2 V)) (p : G.Walk u v) (hu : u = u') (hv : v = v') (h), \\\\ (p.copy hu hv).toDeleteEdges s h = (p.toDeleteEdges s (by subst_vars; exact h)).copy hu hv$$

Lean4

protected theorem toDeleteEdges (s : Set (Sym2 V)) {p : G.Walk v w} (h : p.IsPath) (hp) :
    (p.toDeleteEdges s hp).IsPath :=
  h.transfer _

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