toDeleteEdges — Mathlib

English

If q is a cycle in G, transferring along H with a suitable hp yields a cycle in the transferred graph.

Русский

Если q — цикл в G, перенос через H с подходящим hp даёт цикл в перенесённом графе.

LaTeX

$$$\\\\forall {V} {G} {H} {q : G.Walk u u}, \\\\ q.IsCycle \\\\Rightarrow \\\\forall (hq : \\\\forall (e : Sym2 V), List.instMembership.mem q.edges e \\\\Rightarrow Set.instMembership.mem H.edgeSet e), (q.transfer H hq).IsCycle$$

Lean4

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

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