rotate — Mathlib

English

If c is a cycle, rotating by any vertex in its support yields another cycle.

Русский

Если c является циклом, поворот вокруг любой вершины из поддержки дает новый цикл.

LaTeX

$$p.IsCycle \Rightarrow (p.rotate h).IsCycle$$

Lean4

protected theorem rotate {u v : V} {c : G.Walk v v} (hc : c.IsCycle) (h : u ∈ c.support) : (c.rotate h).IsCycle :=
  by
  refine ⟨hc.isCircuit.rotate _, ?_⟩
  rw [List.IsRotated.nodup_iff (support_rotate _ _)]
  exact hc.support_nodup

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