support_rotate — Mathlib

English

For a closed walk c from v to v and a vertex u in its support, rotating c around u does not change the rotated tail of the support: (c.rotate h).support.tail is a rotation of c.support.tail.

Русский

Для замкнутого обхода c с вершины v к v и вершины u в его опоре вращение c вокруг u не меняет хвост опоры: (c.rotate h).support.tail — это поворот хвоста опоры c.

LaTeX

$$$ (c.rotate h).support.tail ~r c.support.tail $$$

Lean4

@[simp]
theorem support_rotate {u v : V} (c : G.Walk v v) (h : u ∈ c.support) : (c.rotate h).support.tail ~r c.support.tail :=
  by
  simp only [rotate, tail_support_append]
  apply List.IsRotated.trans List.isRotated_append
  rw [← tail_support_append, take_spec]

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