isCycles_spanningCoe_toSubgraph — Mathlib

English

Given a path p from u to v, adding the edge v–u yields a cycle in the subgraph.

Русский

Дано путь p от u к v; добавление ребра v–u образует цикл в подграфе.

LaTeX

$$(p.toSubgraph.spanningCoe \cup edge(v,u)).IsCycles$$

Lean4

theorem isCycles_spanningCoe_toSubgraph {u : V} {p : G.Walk u u} (hpc : p.IsCycle) :
    p.toSubgraph.spanningCoe.IsCycles := by
  intro v hv
  apply hpc.ncard_neighborSet_toSubgraph_eq_two
  obtain ⟨_, hw⟩ := hv
  exact p.mem_verts_toSubgraph.mp <| p.toSubgraph.edge_vert hw

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