rotate_darts — Mathlib

English

Rotation preserves the sequence of edges up to a rotation: (rotate_darts c h).darts ~r c.darts.

Русский

Поворот сохраняет последовательность рёбер вплоть до вращения: (rotate_darts c h).darts ~r c.darts.

LaTeX

$$$ (rotate_darts c h).darts ~r c.darts $$$

Lean4

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

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