toDeleteEdges_copy — Mathlib

English

Deleting a set of edges from a cycle q that are not in the edge set yields a cycle.

Русский

Удаление множества ребер из цикла q не затрагивая ребра, не входящие в edgeSet, сохраняет цикл.

LaTeX

$$$\\\\forall {V} (G : SimpleGraph V) {v : V} {s : Set (Sym2 V)} {p : G.Walk v v}, p.IsCycle \\\\Rightarrow \\\\forall (hp : \\\\forall (e : Sym2 V), List.instMembership.mem p.edges e \\\\Rightarrow Not (Set.instMembership.mem s e)), (SimpleGraph.Walk.toDeleteEdges s p hp).IsCycle$$

Lean4

@[simp]
theorem toDeleteEdges_copy {v u u' v' : 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 :=
  by
  subst_vars
  rfl

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