toSubgraph_rotate — Mathlib

English

Let c be a closed walk in a graph G from a vertex to itself, and let u be a vertex that lies on c. If we rotate the walk about u, the subgraph determined by the rotated walk is the same as that of the original walk.

Русский

Пусть c — циклическая обход в графе G, возвращающийся в исходную вершину; пусть u — вершина, принадлежащая обходу. Тогда поворот обхода вокруг u не меняет подграф, порождаемый обходом.

LaTeX

$$$ (c.rotate(h)).toSubgraph = c.toSubgraph $,$$

Lean4

@[simp]
theorem toSubgraph_rotate [DecidableEq V] (c : G.Walk v v) (h : u ∈ c.support) :
    (c.rotate h).toSubgraph = c.toSubgraph := by
  rw [rotate, toSubgraph_append, sup_comm, ← toSubgraph_append, take_spec]

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